| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | usgrexmpldifpr 29276 | . . 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 |  | usgrexmplef.e | . . 3
⊢ 𝐸 = 〈“{0, 1} {1, 2}
{2, 0} {0, 3}”〉 | 
| 3 |  | prex 5436 | . . . 4
⊢ {0, 1}
∈ V | 
| 4 |  | prex 5436 | . . . 4
⊢ {1, 2}
∈ V | 
| 5 |  | prex 5436 | . . . 4
⊢ {2, 0}
∈ V | 
| 6 |  | prex 5436 | . . . 4
⊢ {0, 3}
∈ V | 
| 7 |  | s4f1o 14958 | . . . 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 693 | . . 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 6846 | . 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 3483 | . . . . . . . . . . . 12
⊢ 𝑝 ∈ V | 
| 13 | 12 | elpr 4649 | . . . . . . . . . . 11
⊢ (𝑝 ∈ {{0, 1}, {1, 2}} ↔
(𝑝 = {0, 1} ∨ 𝑝 = {1, 2})) | 
| 14 |  | 0nn0 12543 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 | 
| 15 |  | 4nn0 12547 | . . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℕ0 | 
| 16 |  | 0re 11264 | . . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ | 
| 17 |  | 4re 12351 | . . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℝ | 
| 18 |  | 4pos 12374 | . . . . . . . . . . . . . . . . 17
⊢ 0 <
4 | 
| 19 | 16, 17, 18 | ltleii 11385 | . . . . . . . . . . . . . . . 16
⊢ 0 ≤
4 | 
| 20 |  | elfz2nn0 13659 | . . . . . . . . . . . . . . . 16
⊢ (0 ∈
(0...4) ↔ (0 ∈ ℕ0 ∧ 4 ∈ ℕ0
∧ 0 ≤ 4)) | 
| 21 | 14, 15, 19, 20 | mpbir3an 1341 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
(0...4) | 
| 22 |  | usgrexmplef.v | . . . . . . . . . . . . . . 15
⊢ 𝑉 = (0...4) | 
| 23 | 21, 22 | eleqtrri 2839 | . . . . . . . . . . . . . 14
⊢ 0 ∈
𝑉 | 
| 24 |  | 1nn0 12544 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 | 
| 25 |  | 1re 11262 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ | 
| 26 |  | 1lt4 12443 | . . . . . . . . . . . . . . . . 17
⊢ 1 <
4 | 
| 27 | 25, 17, 26 | ltleii 11385 | . . . . . . . . . . . . . . . 16
⊢ 1 ≤
4 | 
| 28 |  | elfz2nn0 13659 | . . . . . . . . . . . . . . . 16
⊢ (1 ∈
(0...4) ↔ (1 ∈ ℕ0 ∧ 4 ∈ ℕ0
∧ 1 ≤ 4)) | 
| 29 | 24, 15, 27, 28 | mpbir3an 1341 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
(0...4) | 
| 30 | 29, 22 | eleqtrri 2839 | . . . . . . . . . . . . . 14
⊢ 1 ∈
𝑉 | 
| 31 |  | prelpwi 5451 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ 𝑉 ∧ 1 ∈
𝑉) → {0, 1} ∈
𝒫 𝑉) | 
| 32 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 1} ∈ 𝒫
𝑉)) | 
| 33 | 31, 32 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((0
∈ 𝑉 ∧ 1 ∈
𝑉) → (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉)) | 
| 34 | 23, 30, 33 | mp2an 692 | . . . . . . . . . . . . 13
⊢ (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉) | 
| 35 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = {0, 1} →
(♯‘𝑝) =
(♯‘{0, 1})) | 
| 36 |  | prhash2ex 14439 | . . . . . . . . . . . . . 14
⊢
(♯‘{0, 1}) = 2 | 
| 37 | 35, 36 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑝 = {0, 1} →
(♯‘𝑝) =
2) | 
| 38 | 34, 37 | jca 511 | . . . . . . . . . . . 12
⊢ (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 39 |  | 2nn0 12545 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 | 
| 40 |  | 2re 12341 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ | 
| 41 |  | 2lt4 12442 | . . . . . . . . . . . . . . . . 17
⊢ 2 <
4 | 
| 42 | 40, 17, 41 | ltleii 11385 | . . . . . . . . . . . . . . . 16
⊢ 2 ≤
4 | 
| 43 |  | elfz2nn0 13659 | . . . . . . . . . . . . . . . 16
⊢ (2 ∈
(0...4) ↔ (2 ∈ ℕ0 ∧ 4 ∈ ℕ0
∧ 2 ≤ 4)) | 
| 44 | 39, 15, 42, 43 | mpbir3an 1341 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
(0...4) | 
| 45 | 44, 22 | eleqtrri 2839 | . . . . . . . . . . . . . 14
⊢ 2 ∈
𝑉 | 
| 46 |  | prelpwi 5451 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ 𝑉 ∧ 2 ∈
𝑉) → {1, 2} ∈
𝒫 𝑉) | 
| 47 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ↔ {1, 2} ∈ 𝒫
𝑉)) | 
| 48 | 46, 47 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((1
∈ 𝑉 ∧ 2 ∈
𝑉) → (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉)) | 
| 49 | 30, 45, 48 | mp2an 692 | . . . . . . . . . . . . 13
⊢ (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉) | 
| 50 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = {1, 2} →
(♯‘𝑝) =
(♯‘{1, 2})) | 
| 51 |  | 1ne2 12475 | . . . . . . . . . . . . . . 15
⊢ 1 ≠
2 | 
| 52 |  | 1nn 12278 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ | 
| 53 |  | 2nn 12340 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ | 
| 54 |  | hashprg 14435 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℕ ∧ 2 ∈ ℕ) → (1 ≠ 2 ↔
(♯‘{1, 2}) = 2)) | 
| 55 | 52, 53, 54 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ (1 ≠ 2
↔ (♯‘{1, 2}) = 2) | 
| 56 | 51, 55 | mpbi 230 | . . . . . . . . . . . . . 14
⊢
(♯‘{1, 2}) = 2 | 
| 57 | 50, 56 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑝 = {1, 2} →
(♯‘𝑝) =
2) | 
| 58 | 49, 57 | jca 511 | . . . . . . . . . . . 12
⊢ (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 59 | 38, 58 | jaoi 857 | . . . . . . . . . . 11
⊢ ((𝑝 = {0, 1} ∨ 𝑝 = {1, 2}) → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 60 | 13, 59 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑝 ∈ {{0, 1}, {1, 2}} →
(𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 61 | 12 | elpr 4649 | . . . . . . . . . . 11
⊢ (𝑝 ∈ {{2, 0}, {0, 3}} ↔
(𝑝 = {2, 0} ∨ 𝑝 = {0, 3})) | 
| 62 |  | prelpwi 5451 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ 𝑉 ∧ 0 ∈
𝑉) → {2, 0} ∈
𝒫 𝑉) | 
| 63 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ↔ {2, 0} ∈ 𝒫
𝑉)) | 
| 64 | 62, 63 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((2
∈ 𝑉 ∧ 0 ∈
𝑉) → (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉)) | 
| 65 | 45, 23, 64 | mp2an 692 | . . . . . . . . . . . . 13
⊢ (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉) | 
| 66 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = {2, 0} →
(♯‘𝑝) =
(♯‘{2, 0})) | 
| 67 |  | 2ne0 12371 | . . . . . . . . . . . . . . 15
⊢ 2 ≠
0 | 
| 68 |  | 2z 12651 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ | 
| 69 |  | 0z 12626 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ | 
| 70 |  | hashprg 14435 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℤ ∧ 0 ∈ ℤ) → (2 ≠ 0 ↔
(♯‘{2, 0}) = 2)) | 
| 71 | 68, 69, 70 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ (2 ≠ 0
↔ (♯‘{2, 0}) = 2) | 
| 72 | 67, 71 | mpbi 230 | . . . . . . . . . . . . . 14
⊢
(♯‘{2, 0}) = 2 | 
| 73 | 66, 72 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑝 = {2, 0} →
(♯‘𝑝) =
2) | 
| 74 | 65, 73 | jca 511 | . . . . . . . . . . . 12
⊢ (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 75 |  | 3nn0 12546 | . . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℕ0 | 
| 76 |  | 3re 12347 | . . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℝ | 
| 77 |  | 3lt4 12441 | . . . . . . . . . . . . . . . . 17
⊢ 3 <
4 | 
| 78 | 76, 17, 77 | ltleii 11385 | . . . . . . . . . . . . . . . 16
⊢ 3 ≤
4 | 
| 79 |  | elfz2nn0 13659 | . . . . . . . . . . . . . . . 16
⊢ (3 ∈
(0...4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0
∧ 3 ≤ 4)) | 
| 80 | 75, 15, 78, 79 | mpbir3an 1341 | . . . . . . . . . . . . . . 15
⊢ 3 ∈
(0...4) | 
| 81 | 80, 22 | eleqtrri 2839 | . . . . . . . . . . . . . 14
⊢ 3 ∈
𝑉 | 
| 82 |  | prelpwi 5451 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ 𝑉 ∧ 3 ∈
𝑉) → {0, 3} ∈
𝒫 𝑉) | 
| 83 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 3} ∈ 𝒫
𝑉)) | 
| 84 | 82, 83 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((0
∈ 𝑉 ∧ 3 ∈
𝑉) → (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉)) | 
| 85 | 23, 81, 84 | mp2an 692 | . . . . . . . . . . . . 13
⊢ (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉) | 
| 86 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑝 = {0, 3} →
(♯‘𝑝) =
(♯‘{0, 3})) | 
| 87 |  | 3ne0 12373 | . . . . . . . . . . . . . . . 16
⊢ 3 ≠
0 | 
| 88 | 87 | necomi 2994 | . . . . . . . . . . . . . . 15
⊢ 0 ≠
3 | 
| 89 |  | 3z 12652 | . . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℤ | 
| 90 |  | hashprg 14435 | . . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℤ ∧ 3 ∈ ℤ) → (0 ≠ 3 ↔
(♯‘{0, 3}) = 2)) | 
| 91 | 69, 89, 90 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ (0 ≠ 3
↔ (♯‘{0, 3}) = 2) | 
| 92 | 88, 91 | mpbi 230 | . . . . . . . . . . . . . 14
⊢
(♯‘{0, 3}) = 2 | 
| 93 | 86, 92 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑝 = {0, 3} →
(♯‘𝑝) =
2) | 
| 94 | 85, 93 | jca 511 | . . . . . . . . . . . 12
⊢ (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 95 | 74, 94 | jaoi 857 | . . . . . . . . . . 11
⊢ ((𝑝 = {2, 0} ∨ 𝑝 = {0, 3}) → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 96 | 61, 95 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑝 ∈ {{2, 0}, {0, 3}} →
(𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 97 | 60, 96 | jaoi 857 | . . . . . . . . 9
⊢ ((𝑝 ∈ {{0, 1}, {1, 2}} ∨
𝑝 ∈ {{2, 0}, {0, 3}})
→ (𝑝 ∈ 𝒫
𝑉 ∧
(♯‘𝑝) =
2)) | 
| 98 |  | elun 4152 | . . . . . . . . 9
⊢ (𝑝 ∈ ({{0, 1}, {1, 2}} ∪
{{2, 0}, {0, 3}}) ↔ (𝑝
∈ {{0, 1}, {1, 2}} ∨ 𝑝 ∈ {{2, 0}, {0, 3}})) | 
| 99 |  | fveqeq2 6914 | . . . . . . . . . 10
⊢ (𝑒 = 𝑝 → ((♯‘𝑒) = 2 ↔ (♯‘𝑝) = 2)) | 
| 100 | 99 | elrab 3691 | . . . . . . . . 9
⊢ (𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2)) | 
| 101 | 97, 98, 100 | 3imtr4i 292 | . . . . . . . 8
⊢ (𝑝 ∈ ({{0, 1}, {1, 2}} ∪
{{2, 0}, {0, 3}}) → 𝑝
∈ {𝑒 ∈ 𝒫
𝑉 ∣
(♯‘𝑒) =
2}) | 
| 102 | 101 | ssriv 3986 | . . . . . . 7
⊢ ({{0, 1},
{1, 2}} ∪ {{2, 0}, {0, 3}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} | 
| 103 | 11, 102 | sstrdi 3995 | . . . . . 6
⊢ (ran
𝐸 ⊆ ({{0, 1}, {1, 2}}
∪ {{2, 0}, {0, 3}}) → ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) | 
| 104 | 103 | anim2i 617 | . . . . 5
⊢ ((𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0},
{0, 3}})) → (𝐸 Fn dom
𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})) | 
| 105 |  | df-f 6564 | . . . . 5
⊢ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0,
3}}) ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0},
{0, 3}}))) | 
| 106 |  | df-f 6564 | . . . . 5
⊢ (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})) | 
| 107 | 104, 105,
106 | 3imtr4i 292 | . . . 4
⊢ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0,
3}}) → 𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) | 
| 108 | 107 | anim1i 615 | . . 3
⊢ ((𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0,
3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥) → (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥)) | 
| 109 |  | dff12 6802 | . . 3
⊢ (𝐸:dom 𝐸–1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
↔ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪
{{2, 0}, {0, 3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥)) | 
| 110 |  | dff12 6802 | . . 3
⊢ (𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥)) | 
| 111 | 108, 109,
110 | 3imtr4i 292 | . 2
⊢ (𝐸:dom 𝐸–1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
→ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) | 
| 112 | 9, 10, 111 | mp2b 10 | 1
⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} |