isrusgr0 - Metamath Proof Explorer

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

Theorem isrusgr0 30153

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

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

**Assertion**
Ref	Expression
isrusgr0	⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))

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

**Proof of Theorem isrusgr0**
Step	Hyp	Ref	Expression
1		isrusgr 30148	. 2 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾)))
2		isrusgr0.v	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
3		isrusgr0.d	. . . . 5 ⊢ 𝐷 = (VtxDeg‘𝐺)
4	2, 3	isrgr 30146	. . . 4 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
5	4	anbi2d 642	. . 3 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → ((𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾) ↔ (𝐺 ∈ USGraph ∧ (𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))))
6		3anass 1111	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾) ↔ (𝐺 ∈ USGraph ∧ (𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
7	5, 6	bitr4di 292	. 2 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → ((𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾) ↔ (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
8	1, 7	bitrd 282	1 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 class class class wbr 5102 ‘cfv 6539 ℕ₀^*cxnn0 12683 Vtxcvtx 29580 USGraphcusgr 29736 VtxDegcvtxdg 30052 RegGraph crgr 30142 RegUSGraph crusgr 30143

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-sep 5248 ax-pr 5390

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-iota 6494 df-fv 6547 df-rgr 30144 df-rusgr 30145

This theorem is used by: usgreqdrusgr 30155 cusgrrusgr 30168 rgrusgrprc 30176 rusgrprc 30177

W3C validator