Proof of Theorem usgraop
Step | Hyp | Ref
| Expression |
1 | | df-usgra 25862 |
. . . 4
⊢ USGrph =
{〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}} |
2 | 1 | eleq2i 2680 |
. . 3
⊢ (𝐺 ∈ USGrph ↔ 𝐺 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}}) |
3 | | elopab 4908 |
. . 3
⊢ (𝐺 ∈ {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}} ↔ ∃𝑣∃𝑒(𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2})) |
4 | 2, 3 | bitri 263 |
. 2
⊢ (𝐺 ∈ USGrph ↔
∃𝑣∃𝑒(𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2})) |
5 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
6 | | hasheq0 13015 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ V → ((#‘𝑥) = 0 ↔ 𝑥 = ∅)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑥) = 0
↔ 𝑥 =
∅) |
8 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
9 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑥) = 0
→ 2 ≠ 0) |
10 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑥) = 0
→ (#‘𝑥) =
0) |
11 | 9, 10 | neeqtrrd 2856 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑥) = 0
→ 2 ≠ (#‘𝑥)) |
12 | 11 | necomd 2837 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑥) = 0
→ (#‘𝑥) ≠
2) |
13 | 12 | neneqd 2787 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑥) = 0
→ ¬ (#‘𝑥) =
2) |
14 | 7, 13 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ¬
(#‘𝑥) =
2) |
15 | 14 | con2i 133 |
. . . . . . . . . . . 12
⊢
((#‘𝑥) = 2
→ ¬ 𝑥 =
∅) |
16 | | velsn 4141 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {∅} ↔ 𝑥 = ∅) |
17 | 15, 16 | sylnibr 318 |
. . . . . . . . . . 11
⊢
((#‘𝑥) = 2
→ ¬ 𝑥 ∈
{∅}) |
18 | 17 | biantrud 527 |
. . . . . . . . . 10
⊢
((#‘𝑥) = 2
→ (𝑥 ∈ 𝒫
𝑣 ↔ (𝑥 ∈ 𝒫 𝑣 ∧ ¬ 𝑥 ∈ {∅}))) |
19 | | eldif 3550 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ↔
(𝑥 ∈ 𝒫 𝑣 ∧ ¬ 𝑥 ∈ {∅})) |
20 | 18, 19 | syl6rbbr 278 |
. . . . . . . . 9
⊢
((#‘𝑥) = 2
→ (𝑥 ∈ (𝒫
𝑣 ∖ {∅}) ↔
𝑥 ∈ 𝒫 𝑣)) |
21 | 20 | pm5.32ri 668 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∧
(#‘𝑥) = 2) ↔
(𝑥 ∈ 𝒫 𝑣 ∧ (#‘𝑥) = 2)) |
22 | 21 | abbii 2726 |
. . . . . . 7
⊢ {𝑥 ∣ (𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∧ (#‘𝑥) = 2)} = {𝑥 ∣ (𝑥 ∈ 𝒫 𝑣 ∧ (#‘𝑥) = 2)} |
23 | | df-rab 2905 |
. . . . . . 7
⊢ {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(#‘𝑥) = 2} = {𝑥 ∣ (𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∧ (#‘𝑥) = 2)} |
24 | | df-rab 2905 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2} = {𝑥 ∣ (𝑥 ∈ 𝒫 𝑣 ∧ (#‘𝑥) = 2)} |
25 | 22, 23, 24 | 3eqtr4i 2642 |
. . . . . 6
⊢ {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(#‘𝑥) = 2} = {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2} |
26 | | f1eq3 6011 |
. . . . . 6
⊢ ({𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(#‘𝑥) = 2} = {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2} → (𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2} ↔ 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2})) |
27 | 25, 26 | ax-mp 5 |
. . . . 5
⊢ (𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2} ↔ 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}) |
28 | 27 | biimpi 205 |
. . . 4
⊢ (𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2} → 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}) |
29 | 28 | anim2i 591 |
. . 3
⊢ ((𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}) → (𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2})) |
30 | 29 | 2eximi 1753 |
. 2
⊢
(∃𝑣∃𝑒(𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}) → ∃𝑣∃𝑒(𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2})) |
31 | 4, 30 | sylbi 206 |
1
⊢ (𝐺 ∈ USGrph →
∃𝑣∃𝑒(𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2})) |