rgrprop - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rgrprop		Structured version Visualization version GIF version

Theorem rgrprop 26456

Description: The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.)

**Hypotheses**
Ref	Expression
isrgr.v	⊢ 𝑉 = (Vtx‘𝐺)
isrgr.d	⊢ 𝐷 = (VtxDeg‘𝐺)

**Assertion**
Ref	Expression
rgrprop	⊢ (𝐺 RegGraph 𝐾 → (𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))

Distinct variable groups: 𝑣,𝐺 𝑣,𝐾 Allowed substitution hints: 𝐷(𝑣) 𝑉(𝑣)

Proof of Theorem rgrprop Dummy variables 𝑔 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rgr 26453	. . . 4 ⊢ RegGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ₀^* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}
2	1	breqi 4659	. . 3 ⊢ (𝐺 RegGraph 𝐾 ↔ 𝐺{⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ₀^* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}𝐾)
3		brabv 6699	. . 3 ⊢ (𝐺{⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ₀^* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}𝐾 → (𝐺 ∈ V ∧ 𝐾 ∈ V))
4	2, 3	sylbi 207	. 2 ⊢ (𝐺 RegGraph 𝐾 → (𝐺 ∈ V ∧ 𝐾 ∈ V))
5		isrgr.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
6		isrgr.d	. . . 4 ⊢ 𝐷 = (VtxDeg‘𝐺)
7	5, 6	isrgr 26455	. . 3 ⊢ ((𝐺 ∈ V ∧ 𝐾 ∈ V) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
8	7	biimpd 219	. 2 ⊢ ((𝐺 ∈ V ∧ 𝐾 ∈ V) → (𝐺 RegGraph 𝐾 → (𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
9	4, 8	mpcom 38	1 ⊢ (𝐺 RegGraph 𝐾 → (𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 Vcvv 3200 class class class wbr 4653 {copab 4712 ‘cfv 5888 ℕ₀^*cxnn0 11363 Vtxcvtx 25874 VtxDegcvtxdg 26361 RegGraph crgr 26451

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-iota 5851 df-fv 5896 df-rgr 26453

This theorem is referenced by: rusgrprop0 26463 uhgr0edg0rgrb 26470 frrusgrord 27205

W3C validator