Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . 3
⊢ (∅
USGrph 𝐸 → (∅
∈ V ∧ 𝐸 ∈
V)) |
2 | | isusgra 25873 |
. . . 4
⊢ ((∅
∈ V ∧ 𝐸 ∈ V)
→ (∅ USGrph 𝐸
↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 ∅ ∖ {∅})
∣ (#‘𝑥) =
2})) |
3 | | eqidd 2611 |
. . . . . . 7
⊢ (𝐸 ∈ V → 𝐸 = 𝐸) |
4 | | eqidd 2611 |
. . . . . . 7
⊢ (𝐸 ∈ V → dom 𝐸 = dom 𝐸) |
5 | | pw0 4283 |
. . . . . . . . . . . 12
⊢ 𝒫
∅ = {∅} |
6 | 5 | difeq1i 3686 |
. . . . . . . . . . 11
⊢
(𝒫 ∅ ∖ {∅}) = ({∅} ∖
{∅}) |
7 | | difid 3902 |
. . . . . . . . . . 11
⊢
({∅} ∖ {∅}) = ∅ |
8 | 6, 7 | eqtri 2632 |
. . . . . . . . . 10
⊢
(𝒫 ∅ ∖ {∅}) = ∅ |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ (𝐸 ∈ V → (𝒫
∅ ∖ {∅}) = ∅) |
10 | 9 | rabeqdv 3167 |
. . . . . . . 8
⊢ (𝐸 ∈ V → {𝑥 ∈ (𝒫 ∅
∖ {∅}) ∣ (#‘𝑥) = 2} = {𝑥 ∈ ∅ ∣ (#‘𝑥) = 2}) |
11 | | rab0 3909 |
. . . . . . . 8
⊢ {𝑥 ∈ ∅ ∣
(#‘𝑥) = 2} =
∅ |
12 | 10, 11 | syl6eq 2660 |
. . . . . . 7
⊢ (𝐸 ∈ V → {𝑥 ∈ (𝒫 ∅
∖ {∅}) ∣ (#‘𝑥) = 2} = ∅) |
13 | 3, 4, 12 | f1eq123d 6044 |
. . . . . 6
⊢ (𝐸 ∈ V → (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 ∅ ∖ {∅})
∣ (#‘𝑥) = 2}
↔ 𝐸:dom 𝐸–1-1→∅)) |
14 | | f1f 6014 |
. . . . . . 7
⊢ (𝐸:dom 𝐸–1-1→∅ → 𝐸:dom 𝐸⟶∅) |
15 | | f00 6000 |
. . . . . . . 8
⊢ (𝐸:dom 𝐸⟶∅ ↔ (𝐸 = ∅ ∧ dom 𝐸 = ∅)) |
16 | 15 | simplbi 475 |
. . . . . . 7
⊢ (𝐸:dom 𝐸⟶∅ → 𝐸 = ∅) |
17 | 14, 16 | syl 17 |
. . . . . 6
⊢ (𝐸:dom 𝐸–1-1→∅ → 𝐸 = ∅) |
18 | 13, 17 | syl6bi 242 |
. . . . 5
⊢ (𝐸 ∈ V → (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 ∅ ∖ {∅})
∣ (#‘𝑥) = 2}
→ 𝐸 =
∅)) |
19 | 18 | adantl 481 |
. . . 4
⊢ ((∅
∈ V ∧ 𝐸 ∈ V)
→ (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 ∅ ∖ {∅})
∣ (#‘𝑥) = 2}
→ 𝐸 =
∅)) |
20 | 2, 19 | sylbid 229 |
. . 3
⊢ ((∅
∈ V ∧ 𝐸 ∈ V)
→ (∅ USGrph 𝐸
→ 𝐸 =
∅)) |
21 | 1, 20 | mpcom 37 |
. 2
⊢ (∅
USGrph 𝐸 → 𝐸 = ∅) |
22 | | 0ex 4718 |
. . . 4
⊢ ∅
∈ V |
23 | | usgra0 25899 |
. . . 4
⊢ (∅
∈ V → ∅ USGrph ∅) |
24 | 22, 23 | ax-mp 5 |
. . 3
⊢ ∅
USGrph ∅ |
25 | | breq2 4587 |
. . 3
⊢ (𝐸 = ∅ → (∅
USGrph 𝐸 ↔ ∅
USGrph ∅)) |
26 | 24, 25 | mpbiri 247 |
. 2
⊢ (𝐸 = ∅ → ∅ USGrph
𝐸) |
27 | 21, 26 | impbii 198 |
1
⊢ (∅
USGrph 𝐸 ↔ 𝐸 = ∅) |