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 
|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
Assertion gpgprismgr4cycllem2 
|- Fun `' F

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycllem1.f 
 |-  F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
2 prex 
 |-  { <. 0 , 0 >. , <. 0 , 1 >. } e. _V
3 prex 
 |-  { <. 0 , 1 >. , <. 1 , 1 >. } e. _V
4 2 3 pm3.2i 
 |-  ( { <. 0 , 0 >. , <. 0 , 1 >. } e. _V /\ { <. 0 , 1 >. , <. 1 , 1 >. } e. _V )
5 prex 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } e. _V
6 prex 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } e. _V
7 5 6 pm3.2i 
 |-  ( { <. 1 , 1 >. , <. 1 , 0 >. } e. _V /\ { <. 1 , 0 >. , <. 0 , 0 >. } e. _V )
8 4 7 pm3.2i 
 |-  ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. _V /\ { <. 0 , 1 >. , <. 1 , 1 >. } e. _V ) /\ ( { <. 1 , 1 >. , <. 1 , 0 >. } e. _V /\ { <. 1 , 0 >. , <. 0 , 0 >. } e. _V ) )
9 opex 
 |-  <. 0 , 0 >. e. _V
10 opex 
 |-  <. 0 , 1 >. e. _V
11 9 10 pm3.2i 
 |-  ( <. 0 , 0 >. e. _V /\ <. 0 , 1 >. e. _V )
12 opex 
 |-  <. 1 , 1 >. e. _V
13 10 12 pm3.2i 
 |-  ( <. 0 , 1 >. e. _V /\ <. 1 , 1 >. e. _V )
14 11 13 pm3.2i 
 |-  ( ( <. 0 , 0 >. e. _V /\ <. 0 , 1 >. e. _V ) /\ ( <. 0 , 1 >. e. _V /\ <. 1 , 1 >. e. _V ) )
15 0ne1 
 |-  0 =/= 1
16 15 olci 
 |-  ( 0 =/= 0 \/ 0 =/= 1 )
17 c0ex 
 |-  0 e. _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 >. e. _V /\ <. 0 , 1 >. e. _V ) /\ ( <. 0 , 1 >. e. _V /\ <. 1 , 1 >. e. _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 >. e. _V
28 12 27 pm3.2i 
 |-  ( <. 1 , 1 >. e. _V /\ <. 1 , 0 >. e. _V )
29 11 28 pm3.2i 
 |-  ( ( <. 0 , 0 >. e. _V /\ <. 0 , 1 >. e. _V ) /\ ( <. 1 , 1 >. e. _V /\ <. 1 , 0 >. e. _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 >. e. _V /\ <. 0 , 1 >. e. _V ) /\ ( <. 1 , 1 >. e. _V /\ <. 1 , 0 >. e. _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 >. e. _V /\ <. 0 , 0 >. e. _V )
38 11 37 pm3.2i 
 |-  ( ( <. 0 , 0 >. e. _V /\ <. 0 , 1 >. e. _V ) /\ ( <. 1 , 0 >. e. _V /\ <. 0 , 0 >. e. _V ) )
39 ax-1ne0 
 |-  1 =/= 0
40 39 olci 
 |-  ( 0 =/= 1 \/ 1 =/= 0 )
41 1ex 
 |-  1 e. _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 >. e. _V /\ <. 0 , 1 >. e. _V ) /\ ( <. 1 , 0 >. e. _V /\ <. 0 , 0 >. e. _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 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 1 , 1 >. e. _V /\ <. 1 , 0 >. e. _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 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 1 , 1 >. e. _V /\ <. 1 , 0 >. e. _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 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 1 , 0 >. e. _V /\ <. 0 , 0 >. e. _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 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 1 , 0 >. e. _V /\ <. 0 , 0 >. e. _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 >. e. _V /\ <. 1 , 0 >. e. _V ) /\ ( <. 1 , 0 >. e. _V /\ <. 0 , 0 >. e. _V ) )
72 67 orci 
 |-  ( ( <. 1 , 1 >. =/= <. 1 , 0 >. /\ <. 1 , 1 >. =/= <. 0 , 0 >. ) \/ ( <. 1 , 0 >. =/= <. 1 , 0 >. /\ <. 1 , 0 >. =/= <. 0 , 0 >. ) )
73 prneimg 
 |-  ( ( ( <. 1 , 1 >. e. _V /\ <. 1 , 0 >. e. _V ) /\ ( <. 1 , 0 >. e. _V /\ <. 0 , 0 >. e. _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 >. } e. _V /\ { <. 0 , 1 >. , <. 1 , 1 >. } e. _V ) /\ ( { <. 1 , 1 >. , <. 1 , 0 >. } e. _V /\ { <. 1 , 0 >. , <. 0 , 0 >. } e. _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 >. } e. _V /\ { <. 0 , 1 >. , <. 1 , 1 >. } e. _V ) /\ ( { <. 1 , 1 >. , <. 1 , 0 >. } e. _V /\ { <. 1 , 0 >. , <. 0 , 0 >. } e. _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 >. } ) ) -> ( F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> -> F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) ) )
79 78 imp 
 |-  ( ( ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. _V /\ { <. 0 , 1 >. , <. 1 , 1 >. } e. _V ) /\ ( { <. 1 , 1 >. , <. 1 , 0 >. } e. _V /\ { <. 1 , 0 >. , <. 0 , 0 >. } e. _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 >. } ) ) ) -> ( F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> -> F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) )
80 pm2.27 
 |-  ( F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> -> ( ( F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> -> F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) -> F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) )
81 1 80 ax-mp 
 |-  ( ( F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> -> F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) -> F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) )
82 df-f1o 
 |-  ( F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) <-> ( F : dom F -1-1-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) /\ F : dom F -onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) )
83 df-f1 
 |-  ( F : dom F -1-1-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) <-> ( F : dom F --> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) /\ Fun `' F ) )
84 83 simprbi 
 |-  ( F : dom F -1-1-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) -> Fun `' F )
85 84 adantr 
 |-  ( ( F : dom F -1-1-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) /\ F : dom F -onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) -> Fun `' F )
86 82 85 sylbi 
 |-  ( F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) -> Fun `' F )
87 81 86 syl 
 |-  ( ( F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> -> F : dom F -1-1-onto-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 1 >. , <. 1 , 1 >. } } u. { { <. 1 , 1 >. , <. 1 , 0 >. } , { <. 1 , 0 >. , <. 0 , 0 >. } } ) ) -> Fun `' F )
88 77 79 87 mp2b 
 |-  Fun `' F