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 ( 𝐹 : ( 0 ..^ 3 ) –1-1→ { 𝑋 , 𝑌 , 𝑍 } → ( ( ( ( 𝐹 ‘ 0 ) = 𝑋 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ∧ ( 𝐹 ‘ 2 ) = 𝑍 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑋 ∧ ( 𝐹 ‘ 1 ) = 𝑍 ∧ ( 𝐹 ‘ 2 ) = 𝑌 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑋 ∧ ( 𝐹 ‘ 2 ) = 𝑍 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑍 ∧ ( 𝐹 ‘ 2 ) = 𝑋 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑍 ∧ ( 𝐹 ‘ 1 ) = 𝑋 ∧ ( 𝐹 ‘ 2 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑍 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ∧ ( 𝐹 ‘ 2 ) = 𝑋 ) ) ) )

Proof

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