| Step | Hyp | Ref
| Expression |
| 1 | | lfuhgr1v0e.i |
. . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) |
| 2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ 𝐼 =
(iEdg‘𝐺)) |
| 3 | 1 | dmeqi 5915 |
. . . . . 6
⊢ dom 𝐼 = dom (iEdg‘𝐺) |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ dom 𝐼 = dom
(iEdg‘𝐺)) |
| 5 | | lfuhgr1v0e.e |
. . . . . 6
⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} |
| 6 | | lfuhgr1v0e.v |
. . . . . . . . . 10
⊢ 𝑉 = (Vtx‘𝐺) |
| 7 | 6 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝑉 ∈ V |
| 8 | | hash1snb 14458 |
. . . . . . . . 9
⊢ (𝑉 ∈ V →
((♯‘𝑉) = 1
↔ ∃𝑣 𝑉 = {𝑣})) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . . 8
⊢
((♯‘𝑉) =
1 ↔ ∃𝑣 𝑉 = {𝑣}) |
| 10 | | pweq 4614 |
. . . . . . . . . . . 12
⊢ (𝑉 = {𝑣} → 𝒫 𝑉 = 𝒫 {𝑣}) |
| 11 | 10 | rabeqdv 3452 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (♯‘𝑥)}) |
| 12 | | 2pos 12369 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
| 13 | | 0re 11263 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
| 14 | | 2re 12340 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
| 15 | 13, 14 | ltnlei 11382 |
. . . . . . . . . . . . . . 15
⊢ (0 < 2
↔ ¬ 2 ≤ 0) |
| 16 | 12, 15 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢ ¬ 2
≤ 0 |
| 17 | | 1lt2 12437 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
| 18 | | 1re 11261 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
| 19 | 18, 14 | ltnlei 11382 |
. . . . . . . . . . . . . . 15
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
| 20 | 17, 19 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢ ¬ 2
≤ 1 |
| 21 | | 0ex 5307 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ V |
| 22 | | vsnex 5434 |
. . . . . . . . . . . . . . 15
⊢ {𝑣} ∈ V |
| 23 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
| 24 | | hash0 14406 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘∅) = 0 |
| 25 | 23, 24 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) |
| 26 | 25 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (2 ≤
(♯‘𝑥) ↔ 2
≤ 0)) |
| 27 | 26 | notbid 318 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (¬ 2 ≤
(♯‘𝑥) ↔
¬ 2 ≤ 0)) |
| 28 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = {𝑣} → (♯‘𝑥) = (♯‘{𝑣})) |
| 29 | | hashsng 14408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ V →
(♯‘{𝑣}) =
1) |
| 30 | 29 | elv 3485 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘{𝑣})
= 1 |
| 31 | 28, 30 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = {𝑣} → (♯‘𝑥) = 1) |
| 32 | 31 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = {𝑣} → (2 ≤ (♯‘𝑥) ↔ 2 ≤
1)) |
| 33 | 32 | notbid 318 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑣} → (¬ 2 ≤ (♯‘𝑥) ↔ ¬ 2 ≤
1)) |
| 34 | 21, 22, 27, 33 | ralpr 4700 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
{∅, {𝑣}} ¬ 2 ≤
(♯‘𝑥) ↔
(¬ 2 ≤ 0 ∧ ¬ 2 ≤ 1)) |
| 35 | 16, 20, 34 | mpbir2an 711 |
. . . . . . . . . . . . 13
⊢
∀𝑥 ∈
{∅, {𝑣}} ¬ 2 ≤
(♯‘𝑥) |
| 36 | | pwsn 4900 |
. . . . . . . . . . . . . 14
⊢ 𝒫
{𝑣} = {∅, {𝑣}} |
| 37 | 36 | raleqi 3324 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝒫 {𝑣} ¬ 2 ≤
(♯‘𝑥) ↔
∀𝑥 ∈ {∅,
{𝑣}} ¬ 2 ≤
(♯‘𝑥)) |
| 38 | 35, 37 | mpbir 231 |
. . . . . . . . . . . 12
⊢
∀𝑥 ∈
𝒫 {𝑣} ¬ 2 ≤
(♯‘𝑥) |
| 39 | | rabeq0 4388 |
. . . . . . . . . . . 12
⊢ ({𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤
(♯‘𝑥)} =
∅ ↔ ∀𝑥
∈ 𝒫 {𝑣} ¬
2 ≤ (♯‘𝑥)) |
| 40 | 38, 39 | mpbir 231 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤
(♯‘𝑥)} =
∅ |
| 41 | 11, 40 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = ∅) |
| 42 | 41 | a1d 25 |
. . . . . . . . 9
⊢ (𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = ∅)) |
| 43 | 42 | exlimiv 1930 |
. . . . . . . 8
⊢
(∃𝑣 𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = ∅)) |
| 44 | 9, 43 | sylbi 217 |
. . . . . . 7
⊢
((♯‘𝑉) =
1 → (𝐺 ∈ UHGraph
→ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)} =
∅)) |
| 45 | 44 | impcom 407 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)} =
∅) |
| 46 | 5, 45 | eqtrid 2789 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ 𝐸 =
∅) |
| 47 | 2, 4, 46 | feq123d 6725 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ (𝐼:dom 𝐼⟶𝐸 ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅)) |
| 48 | 47 | biimp3a 1471 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅) |
| 49 | | f00 6790 |
. . . 4
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶∅ ↔ ((iEdg‘𝐺) = ∅ ∧ dom
(iEdg‘𝐺) =
∅)) |
| 50 | 49 | simplbi 497 |
. . 3
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶∅ → (iEdg‘𝐺) = ∅) |
| 51 | 48, 50 | syl 17 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → (iEdg‘𝐺) = ∅) |
| 52 | | uhgriedg0edg0 29144 |
. . 3
⊢ (𝐺 ∈ UHGraph →
((Edg‘𝐺) = ∅
↔ (iEdg‘𝐺) =
∅)) |
| 53 | 52 | 3ad2ant1 1134 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅)) |
| 54 | 51, 53 | mpbird 257 |
1
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → (Edg‘𝐺) = ∅) |