Step | Hyp | Ref
| Expression |
1 | | lfuhgr1v0e.i |
. . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ 𝐼 =
(iEdg‘𝐺)) |
3 | 1 | dmeqi 5476 |
. . . . . 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 | | fvex 6358 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) ∈
V |
8 | 6, 7 | eqeltri 2831 |
. . . . . . . . 9
⊢ 𝑉 ∈ V |
9 | | hash1snb 13395 |
. . . . . . . . 9
⊢ (𝑉 ∈ V →
((♯‘𝑉) = 1
↔ ∃𝑣 𝑉 = {𝑣})) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢
((♯‘𝑉) =
1 ↔ ∃𝑣 𝑉 = {𝑣}) |
11 | | pweq 4301 |
. . . . . . . . . . . 12
⊢ (𝑉 = {𝑣} → 𝒫 𝑉 = 𝒫 {𝑣}) |
12 | 11 | rabeqdv 3330 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (♯‘𝑥)}) |
13 | | 2pos 11300 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
14 | | 0re 10228 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
15 | | 2re 11278 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
16 | 14, 15 | ltnlei 10346 |
. . . . . . . . . . . . . . 15
⊢ (0 < 2
↔ ¬ 2 ≤ 0) |
17 | 13, 16 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ ¬ 2
≤ 0 |
18 | | 1lt2 11382 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
19 | | 1re 10227 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
20 | 19, 15 | ltnlei 10346 |
. . . . . . . . . . . . . . 15
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
21 | 18, 20 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ ¬ 2
≤ 1 |
22 | | 0ex 4938 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ V |
23 | | snex 5053 |
. . . . . . . . . . . . . . 15
⊢ {𝑣} ∈ V |
24 | | fveq2 6348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
25 | | hash0 13346 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘∅) = 0 |
26 | 24, 25 | syl6eq 2806 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) |
27 | 26 | breq2d 4812 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (2 ≤
(♯‘𝑥) ↔ 2
≤ 0)) |
28 | 27 | notbid 307 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (¬ 2 ≤
(♯‘𝑥) ↔
¬ 2 ≤ 0)) |
29 | | fveq2 6348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = {𝑣} → (♯‘𝑥) = (♯‘{𝑣})) |
30 | | vex 3339 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑣 ∈ V |
31 | | hashsng 13347 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ V →
(♯‘{𝑣}) =
1) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘{𝑣})
= 1 |
33 | 29, 32 | syl6eq 2806 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = {𝑣} → (♯‘𝑥) = 1) |
34 | 33 | breq2d 4812 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = {𝑣} → (2 ≤ (♯‘𝑥) ↔ 2 ≤
1)) |
35 | 34 | notbid 307 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑣} → (¬ 2 ≤ (♯‘𝑥) ↔ ¬ 2 ≤
1)) |
36 | 22, 23, 28, 35 | ralpr 4378 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
{∅, {𝑣}} ¬ 2 ≤
(♯‘𝑥) ↔
(¬ 2 ≤ 0 ∧ ¬ 2 ≤ 1)) |
37 | 17, 21, 36 | mpbir2an 993 |
. . . . . . . . . . . . 13
⊢
∀𝑥 ∈
{∅, {𝑣}} ¬ 2 ≤
(♯‘𝑥) |
38 | | pwsn 4576 |
. . . . . . . . . . . . . 14
⊢ 𝒫
{𝑣} = {∅, {𝑣}} |
39 | 38 | raleqi 3277 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝒫 {𝑣} ¬ 2 ≤
(♯‘𝑥) ↔
∀𝑥 ∈ {∅,
{𝑣}} ¬ 2 ≤
(♯‘𝑥)) |
40 | 37, 39 | mpbir 221 |
. . . . . . . . . . . 12
⊢
∀𝑥 ∈
𝒫 {𝑣} ¬ 2 ≤
(♯‘𝑥) |
41 | | rabeq0 4096 |
. . . . . . . . . . . 12
⊢ ({𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤
(♯‘𝑥)} =
∅ ↔ ∀𝑥
∈ 𝒫 {𝑣} ¬
2 ≤ (♯‘𝑥)) |
42 | 40, 41 | mpbir 221 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤
(♯‘𝑥)} =
∅ |
43 | 12, 42 | syl6eq 2806 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = ∅) |
44 | 43 | a1d 25 |
. . . . . . . . 9
⊢ (𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = ∅)) |
45 | 44 | exlimiv 2003 |
. . . . . . . 8
⊢
(∃𝑣 𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} = ∅)) |
46 | 10, 45 | sylbi 207 |
. . . . . . 7
⊢
((♯‘𝑉) =
1 → (𝐺 ∈ UHGraph
→ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)} =
∅)) |
47 | 46 | impcom 445 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)} =
∅) |
48 | 5, 47 | syl5eq 2802 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ 𝐸 =
∅) |
49 | 2, 4, 48 | feq123d 6191 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1)
→ (𝐼:dom 𝐼⟶𝐸 ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅)) |
50 | 49 | biimp3a 1577 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅) |
51 | | f00 6244 |
. . . 4
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶∅ ↔ ((iEdg‘𝐺) = ∅ ∧ dom
(iEdg‘𝐺) =
∅)) |
52 | 51 | simplbi 478 |
. . 3
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶∅ → (iEdg‘𝐺) = ∅) |
53 | 50, 52 | syl 17 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → (iEdg‘𝐺) = ∅) |
54 | | uhgriedg0edg0 26217 |
. . 3
⊢ (𝐺 ∈ UHGraph →
((Edg‘𝐺) = ∅
↔ (iEdg‘𝐺) =
∅)) |
55 | 54 | 3ad2ant1 1128 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅)) |
56 | 53, 55 | mpbird 247 |
1
⊢ ((𝐺 ∈ UHGraph ∧
(♯‘𝑉) = 1 ∧
𝐼:dom 𝐼⟶𝐸) → (Edg‘𝐺) = ∅) |