Step | Hyp | Ref
| Expression |
1 | | lfuhgr1v0e.i |
. . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1) →
𝐼 = (iEdg‘𝐺)) |
3 | 1 | dmeqi 5325 |
. . . . . 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 6201 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) ∈
V |
8 | 6, 7 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝑉 ∈ V |
9 | | hash1snb 13207 |
. . . . . . . . 9
⊢ (𝑉 ∈ V → ((#‘𝑉) = 1 ↔ ∃𝑣 𝑉 = {𝑣})) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢
((#‘𝑉) = 1
↔ ∃𝑣 𝑉 = {𝑣}) |
11 | | pweq 4161 |
. . . . . . . . . . . 12
⊢ (𝑉 = {𝑣} → 𝒫 𝑉 = 𝒫 {𝑣}) |
12 | 11 | rabeqdv 3194 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (#‘𝑥)}) |
13 | | 2pos 11112 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
14 | | 0re 10040 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
15 | | 2re 11090 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
16 | 14, 15 | ltnlei 10158 |
. . . . . . . . . . . . . . 15
⊢ (0 < 2
↔ ¬ 2 ≤ 0) |
17 | 13, 16 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ ¬ 2
≤ 0 |
18 | | 1lt2 11194 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
19 | | 1re 10039 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
20 | 19, 15 | ltnlei 10158 |
. . . . . . . . . . . . . . 15
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
21 | 18, 20 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ ¬ 2
≤ 1 |
22 | | 0ex 4790 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ V |
23 | | snex 4908 |
. . . . . . . . . . . . . . 15
⊢ {𝑣} ∈ V |
24 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ∅ → (#‘𝑥) =
(#‘∅)) |
25 | | hash0 13158 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘∅) = 0 |
26 | 24, 25 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∅ → (#‘𝑥) = 0) |
27 | 26 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (2 ≤
(#‘𝑥) ↔ 2 ≤
0)) |
28 | 27 | notbid 308 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (¬ 2 ≤
(#‘𝑥) ↔ ¬ 2
≤ 0)) |
29 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = {𝑣} → (#‘𝑥) = (#‘{𝑣})) |
30 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑣 ∈ V |
31 | | hashsng 13159 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ V → (#‘{𝑣}) = 1) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘{𝑣}) =
1 |
33 | 29, 32 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = {𝑣} → (#‘𝑥) = 1) |
34 | 33 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = {𝑣} → (2 ≤ (#‘𝑥) ↔ 2 ≤ 1)) |
35 | 34 | notbid 308 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑣} → (¬ 2 ≤ (#‘𝑥) ↔ ¬ 2 ≤
1)) |
36 | 22, 23, 28, 35 | ralpr 4238 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
{∅, {𝑣}} ¬ 2 ≤
(#‘𝑥) ↔ (¬ 2
≤ 0 ∧ ¬ 2 ≤ 1)) |
37 | 17, 21, 36 | mpbir2an 955 |
. . . . . . . . . . . . 13
⊢
∀𝑥 ∈
{∅, {𝑣}} ¬ 2 ≤
(#‘𝑥) |
38 | | pwsn 4428 |
. . . . . . . . . . . . . 14
⊢ 𝒫
{𝑣} = {∅, {𝑣}} |
39 | 38 | raleqi 3142 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝒫 {𝑣} ¬ 2 ≤
(#‘𝑥) ↔
∀𝑥 ∈ {∅,
{𝑣}} ¬ 2 ≤
(#‘𝑥)) |
40 | 37, 39 | mpbir 221 |
. . . . . . . . . . . 12
⊢
∀𝑥 ∈
𝒫 {𝑣} ¬ 2 ≤
(#‘𝑥) |
41 | | rabeq0 3957 |
. . . . . . . . . . . 12
⊢ ({𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (#‘𝑥)} = ∅ ↔
∀𝑥 ∈ 𝒫
{𝑣} ¬ 2 ≤
(#‘𝑥)) |
42 | 40, 41 | mpbir 221 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (#‘𝑥)} = ∅ |
43 | 12, 42 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅) |
44 | 43 | a1d 25 |
. . . . . . . . 9
⊢ (𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅)) |
45 | 44 | exlimiv 1858 |
. . . . . . . 8
⊢
(∃𝑣 𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅)) |
46 | 10, 45 | sylbi 207 |
. . . . . . 7
⊢
((#‘𝑉) = 1
→ (𝐺 ∈ UHGraph
→ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(#‘𝑥)} =
∅)) |
47 | 46 | impcom 446 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1) →
{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅) |
48 | 5, 47 | syl5eq 2668 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1) →
𝐸 =
∅) |
49 | 2, 4, 48 | feq123d 6034 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1) →
(𝐼:dom 𝐼⟶𝐸 ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅)) |
50 | 49 | biimp3a 1432 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅) |
51 | | f00 6087 |
. . . 4
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶∅ ↔ ((iEdg‘𝐺) = ∅ ∧ dom
(iEdg‘𝐺) =
∅)) |
52 | 51 | simplbi 476 |
. . 3
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶∅ → (iEdg‘𝐺) = ∅) |
53 | 50, 52 | syl 17 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (iEdg‘𝐺) = ∅) |
54 | | uhgriedg0edg0 26022 |
. . 3
⊢ (𝐺 ∈ UHGraph →
((Edg‘𝐺) = ∅
↔ (iEdg‘𝐺) =
∅)) |
55 | 54 | 3ad2ant1 1082 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅)) |
56 | 53, 55 | mpbird 247 |
1
⊢ ((𝐺 ∈ UHGraph ∧
(#‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (Edg‘𝐺) = ∅) |