Metamath Proof Explorer

Theorem fvf1tp

Description: Values of a one-to-one function between two sets with three elements. Actually, such a function is a bijection. (Contributed by AV, 23-Jul-2025)

Ref Expression
Assertion fvf1tp 
|- ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> F : ( 0 ..^ 3 ) --> { X , Y , Z } )
2 3nn 
 |-  3 e. NN
3 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 3 ) <-> 3 e. NN )
4 2 3 mpbir 
 |-  0 e. ( 0 ..^ 3 )
5 4 a1i 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> 0 e. ( 0 ..^ 3 ) )
6 1 5 ffvelcdmd 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( F ` 0 ) e. { X , Y , Z } )
7 1nn0 
 |-  1 e. NN0
8 1lt3 
 |-  1 < 3
9 elfzo0 
 |-  ( 1 e. ( 0 ..^ 3 ) <-> ( 1 e. NN0 /\ 3 e. NN /\ 1 < 3 ) )
10 7 2 8 9 mpbir3an 
 |-  1 e. ( 0 ..^ 3 )
11 10 a1i 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> 1 e. ( 0 ..^ 3 ) )
12 1 11 ffvelcdmd 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( F ` 1 ) e. { X , Y , Z } )
13 2nn0 
 |-  2 e. NN0
14 2lt3 
 |-  2 < 3
15 elfzo0 
 |-  ( 2 e. ( 0 ..^ 3 ) <-> ( 2 e. NN0 /\ 3 e. NN /\ 2 < 3 ) )
16 13 2 14 15 mpbir3an 
 |-  2 e. ( 0 ..^ 3 )
17 16 a1i 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> 2 e. ( 0 ..^ 3 ) )
18 1 17 ffvelcdmd 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( F ` 2 ) e. { X , Y , Z } )
19 eltpi 
 |-  ( ( F ` 0 ) e. { X , Y , Z } -> ( ( F ` 0 ) = X \/ ( F ` 0 ) = Y \/ ( F ` 0 ) = Z ) )
20 eltpi 
 |-  ( ( F ` 1 ) e. { X , Y , Z } -> ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) )
21 eltpi 
 |-  ( ( F ` 2 ) e. { X , Y , Z } -> ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) )
22 19 20 21 3anim123i 
 |-  ( ( ( F ` 0 ) e. { X , Y , Z } /\ ( F ` 1 ) e. { X , Y , Z } /\ ( F ` 2 ) e. { X , Y , Z } ) -> ( ( ( F ` 0 ) = X \/ ( F ` 0 ) = Y \/ ( F ` 0 ) = Z ) /\ ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) /\ ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) ) )
23 eqeq2 
 |-  ( X = ( F ` 0 ) -> ( ( F ` 1 ) = X <-> ( F ` 1 ) = ( F ` 0 ) ) )
24 23 eqcoms 
 |-  ( ( F ` 0 ) = X -> ( ( F ` 1 ) = X <-> ( F ` 1 ) = ( F ` 0 ) ) )
25 24 adantl 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 1 ) = X <-> ( F ` 1 ) = ( F ` 0 ) ) )
26 f1veqaeq 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( 1 e. ( 0 ..^ 3 ) /\ 0 e. ( 0 ..^ 3 ) ) ) -> ( ( F ` 1 ) = ( F ` 0 ) -> 1 = 0 ) )
27 10 4 26 mpanr12 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 1 ) = ( F ` 0 ) -> 1 = 0 ) )
28 ax-1ne0 
 |-  1 =/= 0
29 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
30 27 28 29 syl6mpi 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 1 ) = ( F ` 0 ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
31 30 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 1 ) = ( F ` 0 ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
32 25 31 sylbid 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 1 ) = X -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
33 eqeq2 
 |-  ( X = ( F ` 0 ) -> ( ( F ` 2 ) = X <-> ( F ` 2 ) = ( F ` 0 ) ) )
34 33 eqcoms 
 |-  ( ( F ` 0 ) = X -> ( ( F ` 2 ) = X <-> ( F ` 2 ) = ( F ` 0 ) ) )
35 34 adantl 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 2 ) = X <-> ( F ` 2 ) = ( F ` 0 ) ) )
36 16 4 pm3.2i 
 |-  ( 2 e. ( 0 ..^ 3 ) /\ 0 e. ( 0 ..^ 3 ) )
37 36 a1i 
 |-  ( ( F ` 0 ) = X -> ( 2 e. ( 0 ..^ 3 ) /\ 0 e. ( 0 ..^ 3 ) ) )
38 f1veqaeq 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( 2 e. ( 0 ..^ 3 ) /\ 0 e. ( 0 ..^ 3 ) ) ) -> ( ( F ` 2 ) = ( F ` 0 ) -> 2 = 0 ) )
39 37 38 sylan2 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 2 ) = ( F ` 0 ) -> 2 = 0 ) )
40 2ne0 
 |-  2 =/= 0
41 eqneqall 
 |-  ( 2 = 0 -> ( 2 =/= 0 -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
42 39 40 41 syl6mpi 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 2 ) = ( F ` 0 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
43 35 42 sylbid 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
44 43 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
45 eqeq2 
 |-  ( Y = ( F ` 1 ) -> ( ( F ` 2 ) = Y <-> ( F ` 2 ) = ( F ` 1 ) ) )
46 45 eqcoms 
 |-  ( ( F ` 1 ) = Y -> ( ( F ` 2 ) = Y <-> ( F ` 2 ) = ( F ` 1 ) ) )
47 46 adantl 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = Y <-> ( F ` 2 ) = ( F ` 1 ) ) )
48 16 10 pm3.2i 
 |-  ( 2 e. ( 0 ..^ 3 ) /\ 1 e. ( 0 ..^ 3 ) )
49 48 a1i 
 |-  ( ( F ` 0 ) = X -> ( 2 e. ( 0 ..^ 3 ) /\ 1 e. ( 0 ..^ 3 ) ) )
50 f1veqaeq 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( 2 e. ( 0 ..^ 3 ) /\ 1 e. ( 0 ..^ 3 ) ) ) -> ( ( F ` 2 ) = ( F ` 1 ) -> 2 = 1 ) )
51 49 50 sylan2 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 2 ) = ( F ` 1 ) -> 2 = 1 ) )
52 1ne2 
 |-  1 =/= 2
53 52 necomi 
 |-  2 =/= 1
54 eqneqall 
 |-  ( 2 = 1 -> ( 2 =/= 1 -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
55 51 53 54 syl6mpi 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
56 55 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
57 47 56 sylbid 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = Y -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
58 simpllr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = Z ) -> ( F ` 0 ) = X )
59 simplr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = Z ) -> ( F ` 1 ) = Y )
60 simpr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = Z ) -> ( F ` 2 ) = Z )
61 58 59 60 3jca 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = Z ) -> ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) )
62 61 orcd 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = Z ) -> ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) )
63 62 3mix1d 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )
64 63 ex 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = Z -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
65 44 57 64 3jaod 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Y ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
66 65 ex 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 1 ) = Y -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
67 43 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
68 simpllr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = Y ) -> ( F ` 0 ) = X )
69 simplr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = Y ) -> ( F ` 1 ) = Z )
70 simpr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = Y ) -> ( F ` 2 ) = Y )
71 68 69 70 3jca 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = Y ) -> ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) )
72 71 olcd 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = Y ) -> ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) )
73 72 3mix1d 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = Y ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )
74 73 ex 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = Y -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
75 eqeq2 
 |-  ( Z = ( F ` 1 ) -> ( ( F ` 2 ) = Z <-> ( F ` 2 ) = ( F ` 1 ) ) )
76 75 eqcoms 
 |-  ( ( F ` 1 ) = Z -> ( ( F ` 2 ) = Z <-> ( F ` 2 ) = ( F ` 1 ) ) )
77 76 adantl 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = Z <-> ( F ` 2 ) = ( F ` 1 ) ) )
78 16 10 50 mpanr12 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 2 ) = ( F ` 1 ) -> 2 = 1 ) )
79 78 53 54 syl6mpi 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
80 79 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
81 80 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
82 77 81 sylbid 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = Z -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
83 67 74 82 3jaod 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) /\ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
84 83 ex 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( F ` 1 ) = Z -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
85 32 66 84 3jaod 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = X ) -> ( ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
86 85 ex 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 0 ) = X -> ( ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) ) )
87 eqeq2 
 |-  ( X = ( F ` 1 ) -> ( ( F ` 2 ) = X <-> ( F ` 2 ) = ( F ` 1 ) ) )
88 87 eqcoms 
 |-  ( ( F ` 1 ) = X -> ( ( F ` 2 ) = X <-> ( F ` 2 ) = ( F ` 1 ) ) )
89 88 adantl 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = X <-> ( F ` 2 ) = ( F ` 1 ) ) )
90 79 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
91 90 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
92 89 91 sylbid 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
93 eqeq2 
 |-  ( Y = ( F ` 0 ) -> ( ( F ` 2 ) = Y <-> ( F ` 2 ) = ( F ` 0 ) ) )
94 93 eqcoms 
 |-  ( ( F ` 0 ) = Y -> ( ( F ` 2 ) = Y <-> ( F ` 2 ) = ( F ` 0 ) ) )
95 94 adantl 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 2 ) = Y <-> ( F ` 2 ) = ( F ` 0 ) ) )
96 16 4 38 mpanr12 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 2 ) = ( F ` 0 ) -> 2 = 0 ) )
97 96 40 41 syl6mpi 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 2 ) = ( F ` 0 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
98 97 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 2 ) = ( F ` 0 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
99 95 98 sylbid 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 2 ) = Y -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
100 99 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = Y -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
101 simpllr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Z ) -> ( F ` 0 ) = Y )
102 simplr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Z ) -> ( F ` 1 ) = X )
103 simpr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Z ) -> ( F ` 2 ) = Z )
104 101 102 103 3jca 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Z ) -> ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) )
105 104 orcd 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Z ) -> ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) )
106 105 3mix2d 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )
107 106 ex 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = Z -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
108 92 100 107 3jaod 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = X ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
109 108 ex 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 1 ) = X -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
110 eqeq2 
 |-  ( Y = ( F ` 0 ) -> ( ( F ` 1 ) = Y <-> ( F ` 1 ) = ( F ` 0 ) ) )
111 110 eqcoms 
 |-  ( ( F ` 0 ) = Y -> ( ( F ` 1 ) = Y <-> ( F ` 1 ) = ( F ` 0 ) ) )
112 111 adantl 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 1 ) = Y <-> ( F ` 1 ) = ( F ` 0 ) ) )
113 30 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 1 ) = ( F ` 0 ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
114 112 113 sylbid 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 1 ) = Y -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
115 simpllr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = X ) -> ( F ` 0 ) = Y )
116 simplr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = X ) -> ( F ` 1 ) = Z )
117 simpr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = X ) -> ( F ` 2 ) = X )
118 115 116 117 3jca 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = X ) -> ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) )
119 118 olcd 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = X ) -> ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) )
120 119 3mix2d 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) /\ ( F ` 2 ) = X ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )
121 120 ex 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
122 99 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = Y -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
123 76 adantl 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = Z <-> ( F ` 2 ) = ( F ` 1 ) ) )
124 90 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
125 123 124 sylbid 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) -> ( ( F ` 2 ) = Z -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
126 121 122 125 3jaod 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) /\ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
127 126 ex 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( F ` 1 ) = Z -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
128 109 114 127 3jaod 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Y ) -> ( ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
129 128 ex 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 0 ) = Y -> ( ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) ) )
130 88 adantl 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = X <-> ( F ` 2 ) = ( F ` 1 ) ) )
131 79 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
132 130 131 sylbid 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
133 132 adantlr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
134 simpllr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Y ) -> ( F ` 0 ) = Z )
135 simplr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Y ) -> ( F ` 1 ) = X )
136 simpr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Y ) -> ( F ` 2 ) = Y )
137 134 135 136 3jca 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Y ) -> ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) )
138 137 orcd 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Y ) -> ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) )
139 138 3mix3d 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) /\ ( F ` 2 ) = Y ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )
140 139 ex 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = Y -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
141 eqeq2 
 |-  ( Z = ( F ` 0 ) -> ( ( F ` 2 ) = Z <-> ( F ` 2 ) = ( F ` 0 ) ) )
142 141 eqcoms 
 |-  ( ( F ` 0 ) = Z -> ( ( F ` 2 ) = Z <-> ( F ` 2 ) = ( F ` 0 ) ) )
143 142 adantl 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 2 ) = Z <-> ( F ` 2 ) = ( F ` 0 ) ) )
144 97 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 2 ) = ( F ` 0 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
145 143 144 sylbid 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 2 ) = Z -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
146 145 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) -> ( ( F ` 2 ) = Z -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
147 133 140 146 3jaod 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = X ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
148 147 ex 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 1 ) = X -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
149 simpllr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = X ) -> ( F ` 0 ) = Z )
150 simplr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = X ) -> ( F ` 1 ) = Y )
151 simpr 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = X ) -> ( F ` 2 ) = X )
152 149 150 151 3jca 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = X ) -> ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) )
153 152 olcd 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = X ) -> ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) )
154 153 3mix3d 
 |-  ( ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) /\ ( F ` 2 ) = X ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )
155 154 ex 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = X -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
156 46 adantl 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = Y <-> ( F ` 2 ) = ( F ` 1 ) ) )
157 79 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
158 157 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = ( F ` 1 ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
159 156 158 sylbid 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = Y -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
160 145 adantr 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) -> ( ( F ` 2 ) = Z -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
161 155 159 160 3jaod 
 |-  ( ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) /\ ( F ` 1 ) = Y ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
162 161 ex 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 1 ) = Y -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
163 eqeq2 
 |-  ( Z = ( F ` 0 ) -> ( ( F ` 1 ) = Z <-> ( F ` 1 ) = ( F ` 0 ) ) )
164 163 eqcoms 
 |-  ( ( F ` 0 ) = Z -> ( ( F ` 1 ) = Z <-> ( F ` 1 ) = ( F ` 0 ) ) )
165 164 adantl 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 1 ) = Z <-> ( F ` 1 ) = ( F ` 0 ) ) )
166 30 adantr 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 1 ) = ( F ` 0 ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
167 165 166 sylbid 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( F ` 1 ) = Z -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
168 148 162 167 3jaod 
 |-  ( ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } /\ ( F ` 0 ) = Z ) -> ( ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) )
169 168 ex 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( F ` 0 ) = Z -> ( ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) ) )
170 86 129 169 3jaod 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( ( F ` 0 ) = X \/ ( F ` 0 ) = Y \/ ( F ` 0 ) = Z ) -> ( ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) -> ( ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) ) ) )
171 170 3impd 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( ( ( F ` 0 ) = X \/ ( F ` 0 ) = Y \/ ( F ` 0 ) = Z ) /\ ( ( F ` 1 ) = X \/ ( F ` 1 ) = Y \/ ( F ` 1 ) = Z ) /\ ( ( F ` 2 ) = X \/ ( F ` 2 ) = Y \/ ( F ` 2 ) = Z ) ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
172 22 171 syl5 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( ( F ` 0 ) e. { X , Y , Z } /\ ( F ` 1 ) e. { X , Y , Z } /\ ( F ` 2 ) e. { X , Y , Z } ) -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) ) )
173 6 12 18 172 mp3and 
 |-  ( F : ( 0 ..^ 3 ) -1-1-> { X , Y , Z } -> ( ( ( ( F ` 0 ) = X /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = X /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = Y ) ) \/ ( ( ( F ` 0 ) = Y /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Z ) \/ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Z /\ ( F ` 2 ) = X ) ) \/ ( ( ( F ` 0 ) = Z /\ ( F ` 1 ) = X /\ ( F ` 2 ) = Y ) \/ ( ( F ` 0 ) = Z /\ ( F ` 1 ) = Y /\ ( F ` 2 ) = X ) ) ) )