This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrexmpl1lem

Description: Lemma for usgrexmpl1 . (Contributed by AV, 2-Aug-2025)

Ref Expression
Hypotheses usgrexmpl1.v ⊢ 𝑉 = ( 0 ... 5 )
usgrexmpl1.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
Assertion usgrexmpl1lem 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl1.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
3 prex ⊢ { 0 , 1 } ∈ V
4 prex ⊢ { 0 , 2 } ∈ V
5 prex ⊢ { 1 , 2 } ∈ V
6 3 4 5 3pm3.2i ⊢ ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V )
7 prex ⊢ { 0 , 3 } ∈ V
8 prex ⊢ { 3 , 4 } ∈ V
9 prex ⊢ { 3 , 5 } ∈ V
10 prex ⊢ { 4 , 5 } ∈ V
11 8 9 10 3pm3.2i ⊢ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V )
12 6 7 11 3pm3.2i ⊢ ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) )
13 0nn0 ⊢ 0 ∈ ℕ0
14 1nn0 ⊢ 1 ∈ ℕ0
15 13 14 pm3.2i ⊢ ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 )
16 2nn0 ⊢ 2 ∈ ℕ0
17 13 16 pm3.2i ⊢ ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 )
18 15 17 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) )
19 ax-1ne0 ⊢ 1 ≠ 0
20 1ne2 ⊢ 1 ≠ 2
21 19 20 pm3.2i ⊢ ( 1 ≠ 0 ∧ 1 ≠ 2 )
22 21 olci ⊢ ( ( 0 ≠ 0 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 2 ) )
23 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 0 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 2 ) ) → { 0 , 1 } ≠ { 0 , 2 } ) )
24 18 22 23 mp2 ⊢ { 0 , 1 } ≠ { 0 , 2 }
25 14 16 pm3.2i ⊢ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 )
26 15 25 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) )
27 0ne1 ⊢ 0 ≠ 1
28 0ne2 ⊢ 0 ≠ 2
29 27 28 pm3.2i ⊢ ( 0 ≠ 1 ∧ 0 ≠ 2 )
30 29 orci ⊢ ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 1 ∧ 1 ≠ 2 ) )
31 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 1 ∧ 1 ≠ 2 ) ) → { 0 , 1 } ≠ { 1 , 2 } ) )
32 26 30 31 mp2 ⊢ { 0 , 1 } ≠ { 1 , 2 }
33 3nn0 ⊢ 3 ∈ ℕ0
34 13 33 pm3.2i ⊢ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 )
35 15 34 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
36 1re ⊢ 1 ∈ ℝ
37 1lt3 ⊢ 1 < 3
38 36 37 ltneii ⊢ 1 ≠ 3
39 19 38 pm3.2i ⊢ ( 1 ≠ 0 ∧ 1 ≠ 3 )
40 39 olci ⊢ ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 3 ) )
41 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 3 ) ) → { 0 , 1 } ≠ { 0 , 3 } ) )
42 35 40 41 mp2 ⊢ { 0 , 1 } ≠ { 0 , 3 }
43 24 32 42 3pm3.2i ⊢ ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } )
44 4nn0 ⊢ 4 ∈ ℕ0
45 33 44 pm3.2i ⊢ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 )
46 15 45 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) )
47 0re ⊢ 0 ∈ ℝ
48 3pos ⊢ 0 < 3
49 47 48 ltneii ⊢ 0 ≠ 3
50 4pos ⊢ 0 < 4
51 47 50 ltneii ⊢ 0 ≠ 4
52 49 51 pm3.2i ⊢ ( 0 ≠ 3 ∧ 0 ≠ 4 )
53 52 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 1 ≠ 3 ∧ 1 ≠ 4 ) )
54 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 1 ≠ 3 ∧ 1 ≠ 4 ) ) → { 0 , 1 } ≠ { 3 , 4 } ) )
55 46 53 54 mp2 ⊢ { 0 , 1 } ≠ { 3 , 4 }
56 5nn0 ⊢ 5 ∈ ℕ0
57 33 56 pm3.2i ⊢ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 )
58 15 57 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
59 5pos ⊢ 0 < 5
60 47 59 ltneii ⊢ 0 ≠ 5
61 49 60 pm3.2i ⊢ ( 0 ≠ 3 ∧ 0 ≠ 5 )
62 61 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 3 ∧ 1 ≠ 5 ) )
63 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 3 ∧ 1 ≠ 5 ) ) → { 0 , 1 } ≠ { 3 , 5 } ) )
64 58 62 63 mp2 ⊢ { 0 , 1 } ≠ { 3 , 5 }
65 44 56 pm3.2i ⊢ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 )
66 15 65 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
67 51 60 pm3.2i ⊢ ( 0 ≠ 4 ∧ 0 ≠ 5 )
68 67 orci ⊢ ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 4 ∧ 1 ≠ 5 ) )
69 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 4 ∧ 1 ≠ 5 ) ) → { 0 , 1 } ≠ { 4 , 5 } ) )
70 66 68 69 mp2 ⊢ { 0 , 1 } ≠ { 4 , 5 }
71 55 64 70 3pm3.2i ⊢ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } )
72 43 71 pm3.2i ⊢ ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) )
73 17 25 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) )
74 29 orci ⊢ ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 2 ≠ 1 ∧ 2 ≠ 2 ) )
75 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 2 ≠ 1 ∧ 2 ≠ 2 ) ) → { 0 , 2 } ≠ { 1 , 2 } ) )
76 73 74 75 mp2 ⊢ { 0 , 2 } ≠ { 1 , 2 }
77 17 34 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
78 2ne0 ⊢ 2 ≠ 0
79 2re ⊢ 2 ∈ ℝ
80 2lt3 ⊢ 2 < 3
81 79 80 ltneii ⊢ 2 ≠ 3
82 78 81 pm3.2i ⊢ ( 2 ≠ 0 ∧ 2 ≠ 3 )
83 82 olci ⊢ ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) )
84 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) ) → { 0 , 2 } ≠ { 0 , 3 } ) )
85 77 83 84 mp2 ⊢ { 0 , 2 } ≠ { 0 , 3 }
86 76 85 pm3.2i ⊢ ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } )
87 17 45 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) )
88 52 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 4 ) )
89 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 4 ) ) → { 0 , 2 } ≠ { 3 , 4 } ) )
90 87 88 89 mp2 ⊢ { 0 , 2 } ≠ { 3 , 4 }
91 17 57 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
92 61 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 5 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 5 ) )
93 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 5 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 5 ) ) → { 0 , 2 } ≠ { 3 , 5 } ) )
94 91 92 93 mp2 ⊢ { 0 , 2 } ≠ { 3 , 5 }
95 17 65 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
96 67 orci ⊢ ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 2 ≠ 4 ∧ 2 ≠ 5 ) )
97 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 2 ≠ 4 ∧ 2 ≠ 5 ) ) → { 0 , 2 } ≠ { 4 , 5 } ) )
98 95 96 97 mp2 ⊢ { 0 , 2 } ≠ { 4 , 5 }
99 90 94 98 3pm3.2i ⊢ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } )
100 86 99 pm3.2i ⊢ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) )
101 25 34 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
102 39 orci ⊢ ( ( 1 ≠ 0 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) )
103 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 0 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) ) → { 1 , 2 } ≠ { 0 , 3 } ) )
104 101 102 103 mp2 ⊢ { 1 , 2 } ≠ { 0 , 3 }
105 25 45 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) )
106 1lt4 ⊢ 1 < 4
107 36 106 ltneii ⊢ 1 ≠ 4
108 38 107 pm3.2i ⊢ ( 1 ≠ 3 ∧ 1 ≠ 4 )
109 108 orci ⊢ ( ( 1 ≠ 3 ∧ 1 ≠ 4 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 4 ) )
110 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 3 ∧ 1 ≠ 4 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 4 ) ) → { 1 , 2 } ≠ { 3 , 4 } ) )
111 105 109 110 mp2 ⊢ { 1 , 2 } ≠ { 3 , 4 }
112 25 57 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
113 1lt5 ⊢ 1 < 5
114 36 113 ltneii ⊢ 1 ≠ 5
115 38 114 pm3.2i ⊢ ( 1 ≠ 3 ∧ 1 ≠ 5 )
116 115 orci ⊢ ( ( 1 ≠ 3 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 5 ) )
117 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 3 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 5 ) ) → { 1 , 2 } ≠ { 3 , 5 } ) )
118 112 116 117 mp2 ⊢ { 1 , 2 } ≠ { 3 , 5 }
119 25 65 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
120 107 114 pm3.2i ⊢ ( 1 ≠ 4 ∧ 1 ≠ 5 )
121 120 orci ⊢ ( ( 1 ≠ 4 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 4 ∧ 2 ≠ 5 ) )
122 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 4 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 4 ∧ 2 ≠ 5 ) ) → { 1 , 2 } ≠ { 4 , 5 } ) )
123 119 121 122 mp2 ⊢ { 1 , 2 } ≠ { 4 , 5 }
124 111 118 123 3pm3.2i ⊢ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } )
125 104 124 pm3.2i ⊢ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) )
126 72 100 125 3pm3.2i ⊢ ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) )
127 34 45 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) )
128 52 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 3 ≠ 3 ∧ 3 ≠ 4 ) )
129 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 3 ≠ 3 ∧ 3 ≠ 4 ) ) → { 0 , 3 } ≠ { 3 , 4 } ) )
130 127 128 129 mp2 ⊢ { 0 , 3 } ≠ { 3 , 4 }
131 34 57 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
132 61 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 5 ) ∨ ( 3 ≠ 3 ∧ 3 ≠ 5 ) )
133 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 5 ) ∨ ( 3 ≠ 3 ∧ 3 ≠ 5 ) ) → { 0 , 3 } ≠ { 3 , 5 } ) )
134 131 132 133 mp2 ⊢ { 0 , 3 } ≠ { 3 , 5 }
135 34 65 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
136 67 orci ⊢ ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 3 ≠ 4 ∧ 3 ≠ 5 ) )
137 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 3 ≠ 4 ∧ 3 ≠ 5 ) ) → { 0 , 3 } ≠ { 4 , 5 } ) )
138 135 136 137 mp2 ⊢ { 0 , 3 } ≠ { 4 , 5 }
139 130 134 138 3pm3.2i ⊢ ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } )
140 45 57 pm3.2i ⊢ ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
141 3re ⊢ 3 ∈ ℝ
142 3lt4 ⊢ 3 < 4
143 141 142 ltneii ⊢ 3 ≠ 4
144 143 necomi ⊢ 4 ≠ 3
145 4re ⊢ 4 ∈ ℝ
146 4lt5 ⊢ 4 < 5
147 145 146 ltneii ⊢ 4 ≠ 5
148 144 147 pm3.2i ⊢ ( 4 ≠ 3 ∧ 4 ≠ 5 )
149 148 olci ⊢ ( ( 3 ≠ 3 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 3 ∧ 4 ≠ 5 ) )
150 prneimg ⊢ ( ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 3 ≠ 3 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 3 ∧ 4 ≠ 5 ) ) → { 3 , 4 } ≠ { 3 , 5 } ) )
151 140 149 150 mp2 ⊢ { 3 , 4 } ≠ { 3 , 5 }
152 45 65 pm3.2i ⊢ ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
153 3lt5 ⊢ 3 < 5
154 141 153 ltneii ⊢ 3 ≠ 5
155 143 154 pm3.2i ⊢ ( 3 ≠ 4 ∧ 3 ≠ 5 )
156 155 orci ⊢ ( ( 3 ≠ 4 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 4 ∧ 4 ≠ 5 ) )
157 prneimg ⊢ ( ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 3 ≠ 4 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 4 ∧ 4 ≠ 5 ) ) → { 3 , 4 } ≠ { 4 , 5 } ) )
158 152 156 157 mp2 ⊢ { 3 , 4 } ≠ { 4 , 5 }
159 57 65 pm3.2i ⊢ ( ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
160 155 orci ⊢ ( ( 3 ≠ 4 ∧ 3 ≠ 5 ) ∨ ( 5 ≠ 4 ∧ 5 ≠ 5 ) )
161 prneimg ⊢ ( ( ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 3 ≠ 4 ∧ 3 ≠ 5 ) ∨ ( 5 ≠ 4 ∧ 5 ≠ 5 ) ) → { 3 , 5 } ≠ { 4 , 5 } ) )
162 159 160 161 mp2 ⊢ { 3 , 5 } ≠ { 4 , 5 }
163 151 158 162 3pm3.2i ⊢ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } )
164 139 163 pm3.2i ⊢ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) )
165 126 164 pm3.2i ⊢ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) )
166 12 165 pm3.2i ⊢ ( ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) ) ∧ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) ) )
167 s7f1o ⊢ ( ( ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) ) ∧ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) ) ) → ( 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ → 𝐸 : ( 0 ..^ 7 ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) )
168 167 imp ⊢ ( ( ( ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) ) ∧ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) ) ) ∧ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) → 𝐸 : ( 0 ..^ 7 ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
169 s7len ⊢ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) = 7
170 169 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) = ( 0 ..^ 7 )
171 f1oeq2 ⊢ ( ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) = ( 0 ..^ 7 ) → ( 𝐸 : ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ↔ 𝐸 : ( 0 ..^ 7 ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) )
172 170 171 ax-mp ⊢ ( 𝐸 : ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ↔ 𝐸 : ( 0 ..^ 7 ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
173 168 172 sylibr ⊢ ( ( ( ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) ) ∧ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) ) ) ∧ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) → 𝐸 : ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
174 2 dmeqi ⊢ dom 𝐸 = dom ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
175 s7cli ⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ∈ Word V
176 wrddm ⊢ ( ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ∈ Word V → dom ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ = ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) )
177 175 176 ax-mp ⊢ dom ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ = ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) )
178 174 177 eqtri ⊢ dom 𝐸 = ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) )
179 f1oeq2 ⊢ ( dom 𝐸 = ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) → ( 𝐸 : dom 𝐸 –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ↔ 𝐸 : ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) )
180 178 179 ax-mp ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ↔ 𝐸 : ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) ) –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
181 173 180 sylibr ⊢ ( ( ( ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) ) ∧ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) ) ) ∧ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) → 𝐸 : dom 𝐸 –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
182 f1of1 ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) → 𝐸 : dom 𝐸 –1-1→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
183 181 182 syl ⊢ ( ( ( ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) ) ∧ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) ) ) ∧ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) → 𝐸 : dom 𝐸 –1-1→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
184 0elfz ⊢ ( 5 ∈ ℕ0 → 0 ∈ ( 0 ... 5 ) )
185 56 184 ax-mp ⊢ 0 ∈ ( 0 ... 5 )
186 5re ⊢ 5 ∈ ℝ
187 36 186 113 ltleii ⊢ 1 ≤ 5
188 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 5 ) ↔ ( 1 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 1 ≤ 5 ) )
189 14 56 187 188 mpbir3an ⊢ 1 ∈ ( 0 ... 5 )
190 prssi ⊢ ( ( 0 ∈ ( 0 ... 5 ) ∧ 1 ∈ ( 0 ... 5 ) ) → { 0 , 1 } ⊆ ( 0 ... 5 ) )
191 185 189 190 mp2an ⊢ { 0 , 1 } ⊆ ( 0 ... 5 )
192 2lt5 ⊢ 2 < 5
193 79 186 192 ltleii ⊢ 2 ≤ 5
194 elfz2nn0 ⊢ ( 2 ∈ ( 0 ... 5 ) ↔ ( 2 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 2 ≤ 5 ) )
195 16 56 193 194 mpbir3an ⊢ 2 ∈ ( 0 ... 5 )
196 prssi ⊢ ( ( 0 ∈ ( 0 ... 5 ) ∧ 2 ∈ ( 0 ... 5 ) ) → { 0 , 2 } ⊆ ( 0 ... 5 ) )
197 185 195 196 mp2an ⊢ { 0 , 2 } ⊆ ( 0 ... 5 )
198 prssi ⊢ ( ( 1 ∈ ( 0 ... 5 ) ∧ 2 ∈ ( 0 ... 5 ) ) → { 1 , 2 } ⊆ ( 0 ... 5 ) )
199 189 195 198 mp2an ⊢ { 1 , 2 } ⊆ ( 0 ... 5 )
200 sseq1 ⊢ ( 𝑒 = { 0 , 1 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 0 , 1 } ⊆ ( 0 ... 5 ) ) )
201 sseq1 ⊢ ( 𝑒 = { 0 , 2 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 0 , 2 } ⊆ ( 0 ... 5 ) ) )
202 sseq1 ⊢ ( 𝑒 = { 1 , 2 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 1 , 2 } ⊆ ( 0 ... 5 ) ) )
203 200 201 202 raltpg ⊢ ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) → ( ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ ( { 0 , 1 } ⊆ ( 0 ... 5 ) ∧ { 0 , 2 } ⊆ ( 0 ... 5 ) ∧ { 1 , 2 } ⊆ ( 0 ... 5 ) ) ) )
204 6 203 ax-mp ⊢ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ ( { 0 , 1 } ⊆ ( 0 ... 5 ) ∧ { 0 , 2 } ⊆ ( 0 ... 5 ) ∧ { 1 , 2 } ⊆ ( 0 ... 5 ) ) )
205 191 197 199 204 mpbir3an ⊢ ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } 𝑒 ⊆ ( 0 ... 5 )
206 141 186 153 ltleii ⊢ 3 ≤ 5
207 elfz2nn0 ⊢ ( 3 ∈ ( 0 ... 5 ) ↔ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 3 ≤ 5 ) )
208 33 56 206 207 mpbir3an ⊢ 3 ∈ ( 0 ... 5 )
209 prssi ⊢ ( ( 0 ∈ ( 0 ... 5 ) ∧ 3 ∈ ( 0 ... 5 ) ) → { 0 , 3 } ⊆ ( 0 ... 5 ) )
210 185 208 209 mp2an ⊢ { 0 , 3 } ⊆ ( 0 ... 5 )
211 sseq1 ⊢ ( 𝑒 = { 0 , 3 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 0 , 3 } ⊆ ( 0 ... 5 ) ) )
212 7 211 ralsn ⊢ ( ∀ 𝑒 ∈ { { 0 , 3 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ { 0 , 3 } ⊆ ( 0 ... 5 ) )
213 210 212 mpbir ⊢ ∀ 𝑒 ∈ { { 0 , 3 } } 𝑒 ⊆ ( 0 ... 5 )
214 ralunb ⊢ ( ∀ 𝑒 ∈ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) 𝑒 ⊆ ( 0 ... 5 ) ↔ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } 𝑒 ⊆ ( 0 ... 5 ) ∧ ∀ 𝑒 ∈ { { 0 , 3 } } 𝑒 ⊆ ( 0 ... 5 ) ) )
215 205 213 214 mpbir2an ⊢ ∀ 𝑒 ∈ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) 𝑒 ⊆ ( 0 ... 5 )
216 145 186 146 ltleii ⊢ 4 ≤ 5
217 elfz2nn0 ⊢ ( 4 ∈ ( 0 ... 5 ) ↔ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 4 ≤ 5 ) )
218 44 56 216 217 mpbir3an ⊢ 4 ∈ ( 0 ... 5 )
219 prssi ⊢ ( ( 3 ∈ ( 0 ... 5 ) ∧ 4 ∈ ( 0 ... 5 ) ) → { 3 , 4 } ⊆ ( 0 ... 5 ) )
220 208 218 219 mp2an ⊢ { 3 , 4 } ⊆ ( 0 ... 5 )
221 nn0fz0 ⊢ ( 5 ∈ ℕ0 ↔ 5 ∈ ( 0 ... 5 ) )
222 56 221 mpbi ⊢ 5 ∈ ( 0 ... 5 )
223 prssi ⊢ ( ( 3 ∈ ( 0 ... 5 ) ∧ 5 ∈ ( 0 ... 5 ) ) → { 3 , 5 } ⊆ ( 0 ... 5 ) )
224 208 222 223 mp2an ⊢ { 3 , 5 } ⊆ ( 0 ... 5 )
225 prssi ⊢ ( ( 4 ∈ ( 0 ... 5 ) ∧ 5 ∈ ( 0 ... 5 ) ) → { 4 , 5 } ⊆ ( 0 ... 5 ) )
226 218 222 225 mp2an ⊢ { 4 , 5 } ⊆ ( 0 ... 5 )
227 sseq1 ⊢ ( 𝑒 = { 3 , 4 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 3 , 4 } ⊆ ( 0 ... 5 ) ) )
228 sseq1 ⊢ ( 𝑒 = { 3 , 5 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 3 , 5 } ⊆ ( 0 ... 5 ) ) )
229 sseq1 ⊢ ( 𝑒 = { 4 , 5 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 4 , 5 } ⊆ ( 0 ... 5 ) ) )
230 227 228 229 raltpg ⊢ ( ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) → ( ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ ( { 3 , 4 } ⊆ ( 0 ... 5 ) ∧ { 3 , 5 } ⊆ ( 0 ... 5 ) ∧ { 4 , 5 } ⊆ ( 0 ... 5 ) ) ) )
231 11 230 ax-mp ⊢ ( ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ ( { 3 , 4 } ⊆ ( 0 ... 5 ) ∧ { 3 , 5 } ⊆ ( 0 ... 5 ) ∧ { 4 , 5 } ⊆ ( 0 ... 5 ) ) )
232 220 224 226 231 mpbir3an ⊢ ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } 𝑒 ⊆ ( 0 ... 5 )
233 ralunb ⊢ ( ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) 𝑒 ⊆ ( 0 ... 5 ) ↔ ( ∀ 𝑒 ∈ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) 𝑒 ⊆ ( 0 ... 5 ) ∧ ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } 𝑒 ⊆ ( 0 ... 5 ) ) )
234 215 232 233 mpbir2an ⊢ ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) 𝑒 ⊆ ( 0 ... 5 )
235 pwssb ⊢ ( ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ⊆ 𝒫 ( 0 ... 5 ) ↔ ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) 𝑒 ⊆ ( 0 ... 5 ) )
236 234 235 mpbir ⊢ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ⊆ 𝒫 ( 0 ... 5 )
237 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( 0 ... 5 )
238 236 237 sseqtrri ⊢ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ⊆ 𝒫 𝑉
239 prhash2ex ⊢ ( ♯ ‘ { 0 , 1 } ) = 2
240 c0ex ⊢ 0 ∈ V
241 2ex ⊢ 2 ∈ V
242 240 241 28 3pm3.2i ⊢ ( 0 ∈ V ∧ 2 ∈ V ∧ 0 ≠ 2 )
243 hashprb ⊢ ( ( 0 ∈ V ∧ 2 ∈ V ∧ 0 ≠ 2 ) ↔ ( ♯ ‘ { 0 , 2 } ) = 2 )
244 242 243 mpbi ⊢ ( ♯ ‘ { 0 , 2 } ) = 2
245 1ex ⊢ 1 ∈ V
246 245 241 20 3pm3.2i ⊢ ( 1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2 )
247 hashprb ⊢ ( ( 1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2 ) ↔ ( ♯ ‘ { 1 , 2 } ) = 2 )
248 246 247 mpbi ⊢ ( ♯ ‘ { 1 , 2 } ) = 2
249 fveqeq2 ⊢ ( 𝑒 = { 0 , 1 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 0 , 1 } ) = 2 ) )
250 fveqeq2 ⊢ ( 𝑒 = { 0 , 2 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 0 , 2 } ) = 2 ) )
251 fveqeq2 ⊢ ( 𝑒 = { 1 , 2 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 1 , 2 } ) = 2 ) )
252 249 250 251 raltpg ⊢ ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) → ( ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ( ♯ ‘ { 0 , 1 } ) = 2 ∧ ( ♯ ‘ { 0 , 2 } ) = 2 ∧ ( ♯ ‘ { 1 , 2 } ) = 2 ) ) )
253 6 252 ax-mp ⊢ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ( ♯ ‘ { 0 , 1 } ) = 2 ∧ ( ♯ ‘ { 0 , 2 } ) = 2 ∧ ( ♯ ‘ { 1 , 2 } ) = 2 ) )
254 239 244 248 253 mpbir3an ⊢ ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ( ♯ ‘ 𝑒 ) = 2
255 3ex ⊢ 3 ∈ V
256 240 255 49 3pm3.2i ⊢ ( 0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3 )
257 hashprb ⊢ ( ( 0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3 ) ↔ ( ♯ ‘ { 0 , 3 } ) = 2 )
258 256 257 mpbi ⊢ ( ♯ ‘ { 0 , 3 } ) = 2
259 fveqeq2 ⊢ ( 𝑒 = { 0 , 3 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 0 , 3 } ) = 2 ) )
260 7 259 ralsn ⊢ ( ∀ 𝑒 ∈ { { 0 , 3 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 0 , 3 } ) = 2 )
261 258 260 mpbir ⊢ ∀ 𝑒 ∈ { { 0 , 3 } } ( ♯ ‘ 𝑒 ) = 2
262 ralunb ⊢ ( ∀ 𝑒 ∈ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ( ♯ ‘ 𝑒 ) = 2 ↔ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ( ♯ ‘ 𝑒 ) = 2 ∧ ∀ 𝑒 ∈ { { 0 , 3 } } ( ♯ ‘ 𝑒 ) = 2 ) )
263 254 261 262 mpbir2an ⊢ ∀ 𝑒 ∈ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ( ♯ ‘ 𝑒 ) = 2
264 145 elexi ⊢ 4 ∈ V
265 255 264 143 3pm3.2i ⊢ ( 3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4 )
266 hashprb ⊢ ( ( 3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4 ) ↔ ( ♯ ‘ { 3 , 4 } ) = 2 )
267 265 266 mpbi ⊢ ( ♯ ‘ { 3 , 4 } ) = 2
268 186 elexi ⊢ 5 ∈ V
269 255 268 154 3pm3.2i ⊢ ( 3 ∈ V ∧ 5 ∈ V ∧ 3 ≠ 5 )
270 hashprb ⊢ ( ( 3 ∈ V ∧ 5 ∈ V ∧ 3 ≠ 5 ) ↔ ( ♯ ‘ { 3 , 5 } ) = 2 )
271 269 270 mpbi ⊢ ( ♯ ‘ { 3 , 5 } ) = 2
272 264 268 147 3pm3.2i ⊢ ( 4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5 )
273 hashprb ⊢ ( ( 4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5 ) ↔ ( ♯ ‘ { 4 , 5 } ) = 2 )
274 272 273 mpbi ⊢ ( ♯ ‘ { 4 , 5 } ) = 2
275 fveqeq2 ⊢ ( 𝑒 = { 3 , 4 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 3 , 4 } ) = 2 ) )
276 fveqeq2 ⊢ ( 𝑒 = { 3 , 5 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 3 , 5 } ) = 2 ) )
277 fveqeq2 ⊢ ( 𝑒 = { 4 , 5 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 4 , 5 } ) = 2 ) )
278 275 276 277 raltpg ⊢ ( ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) → ( ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ( ♯ ‘ { 3 , 4 } ) = 2 ∧ ( ♯ ‘ { 3 , 5 } ) = 2 ∧ ( ♯ ‘ { 4 , 5 } ) = 2 ) ) )
279 11 278 ax-mp ⊢ ( ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ( ♯ ‘ { 3 , 4 } ) = 2 ∧ ( ♯ ‘ { 3 , 5 } ) = 2 ∧ ( ♯ ‘ { 4 , 5 } ) = 2 ) )
280 267 271 274 279 mpbir3an ⊢ ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ( ♯ ‘ 𝑒 ) = 2
281 ralunb ⊢ ( ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ( ♯ ‘ 𝑒 ) = 2 ↔ ( ∀ 𝑒 ∈ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ( ♯ ‘ 𝑒 ) = 2 ∧ ∀ 𝑒 ∈ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ( ♯ ‘ 𝑒 ) = 2 ) )
282 263 280 281 mpbir2an ⊢ ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ( ♯ ‘ 𝑒 ) = 2
283 ssrab ⊢ ( ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ⊆ 𝒫 𝑉 ∧ ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ( ♯ ‘ 𝑒 ) = 2 ) )
284 238 282 283 mpbir2an ⊢ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }
285 f1ss ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ∧ ( ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 0 , 3 } } ) ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ) → 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
286 183 284 285 sylancl ⊢ ( ( ( ( ( { 0 , 1 } ∈ V ∧ { 0 , 2 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ { 0 , 3 } ∈ V ∧ ( { 3 , 4 } ∈ V ∧ { 3 , 5 } ∈ V ∧ { 4 , 5 } ∈ V ) ) ∧ ( ( ( ( { 0 , 1 } ≠ { 0 , 2 } ∧ { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 0 , 1 } ≠ { 3 , 4 } ∧ { 0 , 1 } ≠ { 3 , 5 } ∧ { 0 , 1 } ≠ { 4 , 5 } ) ) ∧ ( ( { 0 , 2 } ≠ { 1 , 2 } ∧ { 0 , 2 } ≠ { 0 , 3 } ) ∧ ( { 0 , 2 } ≠ { 3 , 4 } ∧ { 0 , 2 } ≠ { 3 , 5 } ∧ { 0 , 2 } ≠ { 4 , 5 } ) ) ∧ ( { 1 , 2 } ≠ { 0 , 3 } ∧ ( { 1 , 2 } ≠ { 3 , 4 } ∧ { 1 , 2 } ≠ { 3 , 5 } ∧ { 1 , 2 } ≠ { 4 , 5 } ) ) ) ∧ ( ( { 0 , 3 } ≠ { 3 , 4 } ∧ { 0 , 3 } ≠ { 3 , 5 } ∧ { 0 , 3 } ≠ { 4 , 5 } ) ∧ ( { 3 , 4 } ≠ { 3 , 5 } ∧ { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 5 } ≠ { 4 , 5 } ) ) ) ) ∧ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ) → 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
287 166 2 286 mp2an ⊢ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }