Metamath Proof Explorer

Theorem gpgprismgr4cycllem2

Description: Lemma 2 for gpgprismgr4cycl0 : the cycle <. P , F >. is proper, i.e., it has no overlapping edges. (Contributed by AV, 2-Nov-2025)

Ref Expression
Hypothesis gpgprismgr4cycllem1.f ⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
Assertion gpgprismgr4cycllem2 Fun ◡ 𝐹

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycllem1.f ⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
2 prex ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V
3 prex ⊢ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ V
4 2 3 pm3.2i ⊢ ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ V )
5 prex ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V
6 prex ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ V
7 5 6 pm3.2i ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V ∧ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ V )
8 4 7 pm3.2i ⊢ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ V ) ∧ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V ∧ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ V ) )
9 opex ⊢ ⟨ 0 , 0 ⟩ ∈ V
10 opex ⊢ ⟨ 0 , 1 ⟩ ∈ V
11 9 10 pm3.2i ⊢ ( ⟨ 0 , 0 ⟩ ∈ V ∧ ⟨ 0 , 1 ⟩ ∈ V )
12 opex ⊢ ⟨ 1 , 1 ⟩ ∈ V
13 10 12 pm3.2i ⊢ ( ⟨ 0 , 1 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V )
14 11 13 pm3.2i ⊢ ( ( ⟨ 0 , 0 ⟩ ∈ V ∧ ⟨ 0 , 1 ⟩ ∈ V ) ∧ ( ⟨ 0 , 1 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) )
15 0ne1 ⊢ 0 ≠ 1
16 15 olci ⊢ ( 0 ≠ 0 ∨ 0 ≠ 1 )
17 c0ex ⊢ 0 ∈ V
18 17 17 opthne ⊢ ( ⟨ 0 , 0 ⟩ ≠ ⟨ 0 , 1 ⟩ ↔ ( 0 ≠ 0 ∨ 0 ≠ 1 ) )
19 16 18 mpbir ⊢ ⟨ 0 , 0 ⟩ ≠ ⟨ 0 , 1 ⟩
20 15 orci ⊢ ( 0 ≠ 1 ∨ 0 ≠ 1 )
21 17 17 opthne ⊢ ( ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ↔ ( 0 ≠ 1 ∨ 0 ≠ 1 ) )
22 20 21 mpbir ⊢ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩
23 19 22 pm3.2i ⊢ ( ⟨ 0 , 0 ⟩ ≠ ⟨ 0 , 1 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ )
24 23 orci ⊢ ( ( ⟨ 0 , 0 ⟩ ≠ ⟨ 0 , 1 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ) ∨ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 1 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ) )
25 prneimg ⊢ ( ( ( ⟨ 0 , 0 ⟩ ∈ V ∧ ⟨ 0 , 1 ⟩ ∈ V ) ∧ ( ⟨ 0 , 1 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ) → ( ( ( ⟨ 0 , 0 ⟩ ≠ ⟨ 0 , 1 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ) ∨ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 1 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ) )
26 14 24 25 mp2 ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ }
27 opex ⊢ ⟨ 1 , 0 ⟩ ∈ V
28 12 27 pm3.2i ⊢ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 1 , 0 ⟩ ∈ V )
29 11 28 pm3.2i ⊢ ( ( ⟨ 0 , 0 ⟩ ∈ V ∧ ⟨ 0 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 1 , 0 ⟩ ∈ V ) )
30 15 orci ⊢ ( 0 ≠ 1 ∨ 0 ≠ 0 )
31 17 17 opthne ⊢ ( ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ ↔ ( 0 ≠ 1 ∨ 0 ≠ 0 ) )
32 30 31 mpbir ⊢ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩
33 22 32 pm3.2i ⊢ ( ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ )
34 33 orci ⊢ ( ( ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ ) ∨ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ) )
35 prneimg ⊢ ( ( ( ⟨ 0 , 0 ⟩ ∈ V ∧ ⟨ 0 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 1 , 0 ⟩ ∈ V ) ) → ( ( ( ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ ) ∨ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ) )
36 29 34 35 mp2 ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ }
37 27 9 pm3.2i ⊢ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 0 , 0 ⟩ ∈ V )
38 11 37 pm3.2i ⊢ ( ( ⟨ 0 , 0 ⟩ ∈ V ∧ ⟨ 0 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 0 , 0 ⟩ ∈ V ) )
39 ax-1ne0 ⊢ 1 ≠ 0
40 39 olci ⊢ ( 0 ≠ 1 ∨ 1 ≠ 0 )
41 1ex ⊢ 1 ∈ V
42 17 41 opthne ⊢ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ↔ ( 0 ≠ 1 ∨ 1 ≠ 0 ) )
43 40 42 mpbir ⊢ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩
44 39 olci ⊢ ( 0 ≠ 0 ∨ 1 ≠ 0 )
45 17 41 opthne ⊢ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ↔ ( 0 ≠ 0 ∨ 1 ≠ 0 ) )
46 44 45 mpbir ⊢ ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩
47 43 46 pm3.2i ⊢ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ )
48 47 olci ⊢ ( ( ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ∨ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) )
49 prneimg ⊢ ( ( ( ⟨ 0 , 0 ⟩ ∈ V ∧ ⟨ 0 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 0 , 0 ⟩ ∈ V ) ) → ( ( ( ⟨ 0 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 0 , 0 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ∨ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) )
50 38 48 49 mp2 ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ }
51 26 36 50 3pm3.2i ⊢ ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } )
52 13 28 pm3.2i ⊢ ( ( ⟨ 0 , 1 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 1 , 0 ⟩ ∈ V ) )
53 15 orci ⊢ ( 0 ≠ 1 ∨ 1 ≠ 1 )
54 17 41 opthne ⊢ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ↔ ( 0 ≠ 1 ∨ 1 ≠ 1 ) )
55 53 54 mpbir ⊢ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩
56 55 43 pm3.2i ⊢ ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ )
57 56 orci ⊢ ( ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ) ∨ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ) )
58 prneimg ⊢ ( ( ( ⟨ 0 , 1 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 1 , 0 ⟩ ∈ V ) ) → ( ( ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ) ∨ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ) )
59 52 57 58 mp2 ⊢ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ }
60 13 37 pm3.2i ⊢ ( ( ⟨ 0 , 1 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 0 , 0 ⟩ ∈ V ) )
61 39 olci ⊢ ( 1 ≠ 1 ∨ 1 ≠ 0 )
62 41 41 opthne ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ↔ ( 1 ≠ 1 ∨ 1 ≠ 0 ) )
63 61 62 mpbir ⊢ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩
64 39 olci ⊢ ( 1 ≠ 0 ∨ 1 ≠ 0 )
65 41 41 opthne ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ↔ ( 1 ≠ 0 ∨ 1 ≠ 0 ) )
66 64 65 mpbir ⊢ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩
67 63 66 pm3.2i ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ )
68 67 olci ⊢ ( ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ∨ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) )
69 prneimg ⊢ ( ( ( ⟨ 0 , 1 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 0 , 0 ⟩ ∈ V ) ) → ( ( ( ⟨ 0 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 0 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ∨ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) )
70 60 68 69 mp2 ⊢ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ }
71 28 37 pm3.2i ⊢ ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 1 , 0 ⟩ ∈ V ) ∧ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 0 , 0 ⟩ ∈ V ) )
72 67 orci ⊢ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ∨ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 0 ⟩ ) )
73 prneimg ⊢ ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 1 , 0 ⟩ ∈ V ) ∧ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 0 , 0 ⟩ ∈ V ) ) → ( ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ∨ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 0 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 0 ⟩ ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) )
74 71 72 73 mp2 ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ }
75 59 70 74 3pm3.2i ⊢ ( { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } )
76 51 75 pm3.2i ⊢ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) ∧ ( { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) )
77 8 76 pm3.2i ⊢ ( ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ V ) ∧ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V ∧ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ V ) ) ∧ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) ∧ ( { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) ) )
78 s4f1o ⊢ ( ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ V ) ∧ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V ∧ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ V ) ) → ( ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) ∧ ( { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) ) → ( 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ → 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) ) )
79 78 imp ⊢ ( ( ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ V ) ∧ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V ∧ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ V ) ) ∧ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) ∧ ( { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∧ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ≠ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ) ) ) → ( 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ → 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) )
80 pm2.27 ⊢ ( 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ → ( ( 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ → 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) → 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) )
81 1 80 ax-mp ⊢ ( ( 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ → 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) → 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) )
82 df-f1o ⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ↔ ( 𝐹 : dom 𝐹 –1-1→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ∧ 𝐹 : dom 𝐹 –onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) )
83 df-f1 ⊢ ( 𝐹 : dom 𝐹 –1-1→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ↔ ( 𝐹 : dom 𝐹 ⟶ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ∧ Fun ◡ 𝐹 ) )
84 83 simprbi ⊢ ( 𝐹 : dom 𝐹 –1-1→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) → Fun ◡ 𝐹 )
85 84 adantr ⊢ ( ( 𝐹 : dom 𝐹 –1-1→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ∧ 𝐹 : dom 𝐹 –onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) → Fun ◡ 𝐹 )
86 82 85 sylbi ⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) → Fun ◡ 𝐹 )
87 81 86 syl ⊢ ( ( 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ → 𝐹 : dom 𝐹 –1-1-onto→ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } , { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } } ) ) → Fun ◡ 𝐹 )
88 77 79 87 mp2b ⊢ Fun ◡ 𝐹