Step | Hyp | Ref
| Expression |
1 | | usgraexmpldifpr 25928 |
. . 3
⊢ (({0, 1}
≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2}
≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0,
3})) |
2 | | usgraexmpl.e |
. . 3
⊢ 𝐸 = 〈“{0, 1} {1, 2}
{2, 0} {0, 3}”〉 |
3 | | prex 4836 |
. . . 4
⊢ {0, 1}
∈ V |
4 | | prex 4836 |
. . . 4
⊢ {1, 2}
∈ V |
5 | | prex 4836 |
. . . 4
⊢ {2, 0}
∈ V |
6 | | prex 4836 |
. . . 4
⊢ {0, 3}
∈ V |
7 | | s4f1o 13513 |
. . . 4
⊢ ((({0, 1}
∈ V ∧ {1, 2} ∈ V) ∧ ({2, 0} ∈ V ∧ {0, 3} ∈ V))
→ ((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3})
∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}))
→ (𝐸 =
〈“{0, 1} {1, 2} {2, 0} {0, 3}”〉 → 𝐸:dom 𝐸–1-1-onto→({{0,
1}, {1, 2}} ∪ {{2, 0}, {0, 3}})))) |
8 | 3, 4, 5, 6, 7 | mp4an 705 |
. . 3
⊢ ((({0, 1}
≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2}
≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3})) → (𝐸 = 〈“{0, 1} {1, 2}
{2, 0} {0, 3}”〉 → 𝐸:dom 𝐸–1-1-onto→({{0,
1}, {1, 2}} ∪ {{2, 0}, {0, 3}}))) |
9 | 1, 2, 8 | mp2 9 |
. 2
⊢ 𝐸:dom 𝐸–1-1-onto→({{0,
1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) |
10 | | f1of1 6049 |
. 2
⊢ (𝐸:dom 𝐸–1-1-onto→({{0,
1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝐸:dom 𝐸–1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0,
3}})) |
11 | | id 22 |
. . . . . . 7
⊢ (ran
𝐸 ⊆ ({{0, 1}, {1, 2}}
∪ {{2, 0}, {0, 3}}) → ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0},
{0, 3}})) |
12 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑝 ∈ V |
13 | 12 | elpr 4146 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ {{0, 1}, {1, 2}} ↔
(𝑝 = {0, 1} ∨ 𝑝 = {1, 2})) |
14 | | usgraexmpl.v |
. . . . . . . . . . . . . . 15
⊢ 𝑉 = (0...4) |
15 | 14 | usgraex0elv 25924 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
𝑉 |
16 | 14 | usgraex1elv 25925 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
𝑉 |
17 | | prelpwi 4842 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ 𝑉 ∧ 1 ∈
𝑉) → {0, 1} ∈
𝒫 𝑉) |
18 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 1} ∈ 𝒫
𝑉)) |
19 | 17, 18 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ 𝑉 ∧ 1 ∈
𝑉) → (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉)) |
20 | 15, 16, 19 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = {0, 1} → (#‘𝑝) = (#‘{0,
1})) |
22 | | prhash2ex 13048 |
. . . . . . . . . . . . . 14
⊢
(#‘{0, 1}) = 2 |
23 | 21, 22 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {0, 1} → (#‘𝑝) = 2) |
24 | 20, 23 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
25 | 14 | usgraex2elv 25926 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
𝑉 |
26 | | prelpwi 4842 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ 𝑉 ∧ 2 ∈
𝑉) → {1, 2} ∈
𝒫 𝑉) |
27 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ↔ {1, 2} ∈ 𝒫
𝑉)) |
28 | 26, 27 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ 𝑉 ∧ 2 ∈
𝑉) → (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉)) |
29 | 16, 25, 28 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉) |
30 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = {1, 2} → (#‘𝑝) = (#‘{1,
2})) |
31 | | 1ne2 11117 |
. . . . . . . . . . . . . . 15
⊢ 1 ≠
2 |
32 | | 1nn 10908 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ |
33 | | 2nn 11062 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
34 | | hashprgOLD 13044 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℕ ∧ 2 ∈ ℕ) → (1 ≠ 2 ↔ (#‘{1, 2})
= 2)) |
35 | 32, 33, 34 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (1 ≠ 2
↔ (#‘{1, 2}) = 2) |
36 | 31, 35 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢
(#‘{1, 2}) = 2 |
37 | 30, 36 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {1, 2} → (#‘𝑝) = 2) |
38 | 29, 37 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
39 | 24, 38 | jaoi 393 |
. . . . . . . . . . 11
⊢ ((𝑝 = {0, 1} ∨ 𝑝 = {1, 2}) → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
40 | 13, 39 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑝 ∈ {{0, 1}, {1, 2}} →
(𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
41 | 12 | elpr 4146 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ {{2, 0}, {0, 3}} ↔
(𝑝 = {2, 0} ∨ 𝑝 = {0, 3})) |
42 | | prelpwi 4842 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ 𝑉 ∧ 0 ∈
𝑉) → {2, 0} ∈
𝒫 𝑉) |
43 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ↔ {2, 0} ∈ 𝒫
𝑉)) |
44 | 42, 43 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ 𝑉 ∧ 0 ∈
𝑉) → (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉)) |
45 | 25, 15, 44 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉) |
46 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = {2, 0} → (#‘𝑝) = (#‘{2,
0})) |
47 | | 2ne0 10990 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
48 | | 2z 11286 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
49 | | 0z 11265 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
50 | | hashprgOLD 13044 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℤ ∧ 0 ∈ ℤ) → (2 ≠ 0 ↔ (#‘{2, 0})
= 2)) |
51 | 48, 49, 50 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (2 ≠ 0
↔ (#‘{2, 0}) = 2) |
52 | 47, 51 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢
(#‘{2, 0}) = 2 |
53 | 46, 52 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {2, 0} → (#‘𝑝) = 2) |
54 | 45, 53 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
55 | 14 | usgraex3elv 25927 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
𝑉 |
56 | | prelpwi 4842 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ 𝑉 ∧ 3 ∈
𝑉) → {0, 3} ∈
𝒫 𝑉) |
57 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 3} ∈ 𝒫
𝑉)) |
58 | 56, 57 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ 𝑉 ∧ 3 ∈
𝑉) → (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉)) |
59 | 15, 55, 58 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = {0, 3} → (#‘𝑝) = (#‘{0,
3})) |
61 | | 3ne0 10992 |
. . . . . . . . . . . . . . . 16
⊢ 3 ≠
0 |
62 | 61 | necomi 2836 |
. . . . . . . . . . . . . . 15
⊢ 0 ≠
3 |
63 | | 3z 11287 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℤ |
64 | | hashprgOLD 13044 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℤ ∧ 3 ∈ ℤ) → (0 ≠ 3 ↔ (#‘{0, 3})
= 2)) |
65 | 49, 63, 64 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (0 ≠ 3
↔ (#‘{0, 3}) = 2) |
66 | 62, 65 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢
(#‘{0, 3}) = 2 |
67 | 60, 66 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {0, 3} → (#‘𝑝) = 2) |
68 | 59, 67 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
69 | 54, 68 | jaoi 393 |
. . . . . . . . . . 11
⊢ ((𝑝 = {2, 0} ∨ 𝑝 = {0, 3}) → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
70 | 41, 69 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑝 ∈ {{2, 0}, {0, 3}} →
(𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
71 | 40, 70 | jaoi 393 |
. . . . . . . . 9
⊢ ((𝑝 ∈ {{0, 1}, {1, 2}} ∨
𝑝 ∈ {{2, 0}, {0, 3}})
→ (𝑝 ∈ 𝒫
𝑉 ∧ (#‘𝑝) = 2)) |
72 | | elun 3715 |
. . . . . . . . 9
⊢ (𝑝 ∈ ({{0, 1}, {1, 2}} ∪
{{2, 0}, {0, 3}}) ↔ (𝑝
∈ {{0, 1}, {1, 2}} ∨ 𝑝 ∈ {{2, 0}, {0, 3}})) |
73 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑝 → (#‘𝑒) = (#‘𝑝)) |
74 | 73 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑝 → ((#‘𝑒) = 2 ↔ (#‘𝑝) = 2)) |
75 | 74 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ↔ (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2)) |
76 | 71, 72, 75 | 3imtr4i 280 |
. . . . . . . 8
⊢ (𝑝 ∈ ({{0, 1}, {1, 2}} ∪
{{2, 0}, {0, 3}}) → 𝑝
∈ {𝑒 ∈ 𝒫
𝑉 ∣ (#‘𝑒) = 2}) |
77 | 76 | ssriv 3572 |
. . . . . . 7
⊢ ({{0, 1},
{1, 2}} ∪ {{2, 0}, {0, 3}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} |
78 | 11, 77 | syl6ss 3580 |
. . . . . 6
⊢ (ran
𝐸 ⊆ ({{0, 1}, {1, 2}}
∪ {{2, 0}, {0, 3}}) → ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}) |
79 | 78 | anim2i 591 |
. . . . 5
⊢ ((𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0},
{0, 3}})) → (𝐸 Fn dom
𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2})) |
80 | | df-f 5808 |
. . . . 5
⊢ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0,
3}}) ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0},
{0, 3}}))) |
81 | | df-f 5808 |
. . . . 5
⊢ (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2})) |
82 | 79, 80, 81 | 3imtr4i 280 |
. . . 4
⊢ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0,
3}}) → 𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}) |
83 | 82 | anim1i 590 |
. . 3
⊢ ((𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0,
3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥) → (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥)) |
84 | | dff12 6013 |
. . 3
⊢ (𝐸:dom 𝐸–1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
↔ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪
{{2, 0}, {0, 3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥)) |
85 | | dff12 6013 |
. . 3
⊢ (𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ↔ (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥)) |
86 | 83, 84, 85 | 3imtr4i 280 |
. 2
⊢ (𝐸:dom 𝐸–1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
→ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}) |
87 | 9, 10, 86 | mp2b 10 |
1
⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} |