Step |
Hyp |
Ref |
Expression |
1 |
|
cusgrrusgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝐺 ∈ ComplUSGraph ) |
3 |
1
|
fusgrvtxfi |
⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin ) |
4 |
3
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ∈ Fin ) |
5 |
4
|
adantr |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝑉 ∈ Fin ) |
6 |
|
simpr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ≠ ∅ ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝑉 ≠ ∅ ) |
8 |
1
|
cusgrrusgr |
⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) |
9 |
2 5 7 8
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) |
10 |
9
|
ex |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) ) |
11 |
|
eqid |
⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 ) |
12 |
1 11
|
rusgrprop0 |
⊢ ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → ( 𝐺 ∈ USGraph ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ) |
13 |
12
|
simp3d |
⊢ ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) |
14 |
1
|
vdiscusgr |
⊢ ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) ) |
15 |
14
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) ) |
16 |
13 15
|
syl5 |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) ) |
17 |
10 16
|
impbid |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) ) |