Metamath Proof Explorer

Theorem f13dfv

Description: A one-to-one function with a domain with at least three different elements in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018)

Ref Expression
Hypothesis f13dfv.a ⊢ 𝐴 = { 𝑋 , 𝑌 , 𝑍 }
Assertion f13dfv ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 f13dfv.a ⊢ 𝐴 = { 𝑋 , 𝑌 , 𝑍 }
2 dff14b ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
3 1 raleqi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ { 𝑋 , 𝑌 , 𝑍 } ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) )
4 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
5 4 difeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∖ { 𝑥 } ) = ( 𝐴 ∖ { 𝑋 } ) )
6 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
7 6 neeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
8 5 7 raleqbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
9 sneq ⊢ ( 𝑥 = 𝑌 → { 𝑥 } = { 𝑌 } )
10 9 difeq2d ⊢ ( 𝑥 = 𝑌 → ( 𝐴 ∖ { 𝑥 } ) = ( 𝐴 ∖ { 𝑌 } ) )
11 fveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑌 ) )
12 11 neeq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
13 10 12 raleqbidv ⊢ ( 𝑥 = 𝑌 → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
14 sneq ⊢ ( 𝑥 = 𝑍 → { 𝑥 } = { 𝑍 } )
15 14 difeq2d ⊢ ( 𝑥 = 𝑍 → ( 𝐴 ∖ { 𝑥 } ) = ( 𝐴 ∖ { 𝑍 } ) )
16 fveq2 ⊢ ( 𝑥 = 𝑍 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑍 ) )
17 16 neeq1d ⊢ ( 𝑥 = 𝑍 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
18 15 17 raleqbidv ⊢ ( 𝑥 = 𝑍 → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑍 } ) ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
19 8 13 18 raltpg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 , 𝑍 } ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑍 } ) ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) )
20 19 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 , 𝑍 } ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑍 } ) ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) )
21 1 difeq1i ⊢ ( 𝐴 ∖ { 𝑋 } ) = ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑋 } )
22 tprot ⊢ { 𝑋 , 𝑌 , 𝑍 } = { 𝑌 , 𝑍 , 𝑋 }
23 22 difeq1i ⊢ ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑋 } ) = ( { 𝑌 , 𝑍 , 𝑋 } ∖ { 𝑋 } )
24 necom ⊢ ( 𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋 )
25 necom ⊢ ( 𝑋 ≠ 𝑍 ↔ 𝑍 ≠ 𝑋 )
26 24 25 anbi12i ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ) ↔ ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) )
27 26 biimpi ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ) → ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) )
28 27 3adant3 ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) )
29 diftpsn3 ⊢ ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → ( { 𝑌 , 𝑍 , 𝑋 } ∖ { 𝑋 } ) = { 𝑌 , 𝑍 } )
30 28 29 syl ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑌 , 𝑍 , 𝑋 } ∖ { 𝑋 } ) = { 𝑌 , 𝑍 } )
31 23 30 eqtrid ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑋 } ) = { 𝑌 , 𝑍 } )
32 21 31 eqtrid ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( 𝐴 ∖ { 𝑋 } ) = { 𝑌 , 𝑍 } )
33 32 adantl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐴 ∖ { 𝑋 } ) = { 𝑌 , 𝑍 } )
34 33 raleqdv ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑌 , 𝑍 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
35 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
36 35 neeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
37 fveq2 ⊢ ( 𝑦 = 𝑍 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑍 ) )
38 37 neeq2d ⊢ ( 𝑦 = 𝑍 → ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
39 36 38 ralprg ⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ { 𝑌 , 𝑍 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
40 39 3adant1 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ { 𝑌 , 𝑍 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
41 40 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ { 𝑌 , 𝑍 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
42 34 41 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
43 1 difeq1i ⊢ ( 𝐴 ∖ { 𝑌 } ) = ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑌 } )
44 tpcomb ⊢ { 𝑋 , 𝑌 , 𝑍 } = { 𝑋 , 𝑍 , 𝑌 }
45 44 difeq1i ⊢ ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑌 } ) = ( { 𝑋 , 𝑍 , 𝑌 } ∖ { 𝑌 } )
46 necom ⊢ ( 𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌 )
47 46 biimpi ⊢ ( 𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌 )
48 47 anim2i ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌 ) )
49 48 3adant2 ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌 ) )
50 diftpsn3 ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌 ) → ( { 𝑋 , 𝑍 , 𝑌 } ∖ { 𝑌 } ) = { 𝑋 , 𝑍 } )
51 49 50 syl ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑋 , 𝑍 , 𝑌 } ∖ { 𝑌 } ) = { 𝑋 , 𝑍 } )
52 45 51 eqtrid ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑌 } ) = { 𝑋 , 𝑍 } )
53 43 52 eqtrid ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( 𝐴 ∖ { 𝑌 } ) = { 𝑋 , 𝑍 } )
54 53 adantl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐴 ∖ { 𝑌 } ) = { 𝑋 , 𝑍 } )
55 54 raleqdv ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑋 , 𝑍 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
56 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
57 56 neeq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
58 37 neeq2d ⊢ ( 𝑦 = 𝑍 → ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
59 57 58 ralprg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑍 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
60 59 3adant2 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑍 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
61 60 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑍 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
62 55 61 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
63 1 difeq1i ⊢ ( 𝐴 ∖ { 𝑍 } ) = ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑍 } )
64 diftpsn3 ⊢ ( ( 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑍 } ) = { 𝑋 , 𝑌 } )
65 64 3adant1 ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑋 , 𝑌 , 𝑍 } ∖ { 𝑍 } ) = { 𝑋 , 𝑌 } )
66 63 65 eqtrid ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( 𝐴 ∖ { 𝑍 } ) = { 𝑋 , 𝑌 } )
67 66 adantl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐴 ∖ { 𝑍 } ) = { 𝑋 , 𝑌 } )
68 67 raleqdv ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑍 } ) ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
69 56 neeq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
70 35 neeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
71 69 70 ralprg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
72 71 3adant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
73 72 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
74 68 73 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑍 } ) ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
75 42 62 74 3anbi123d ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑍 } ) ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) ) )
76 ancom ⊢ ( ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ↔ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
77 76 3anbi2i ⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
78 3an6 ⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
79 3anrot ⊢ ( ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
80 79 bicomi ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ) ↔ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
81 necom ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ↔ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) )
82 necom ⊢ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) )
83 necom ⊢ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) )
84 81 82 83 3anbi123i ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
85 80 84 anbi12i ⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
86 anidm ⊢ ( ( ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) ↔ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
87 3ancoma ⊢ ( ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
88 necom ⊢ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) )
89 88 3anbi2i ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
90 87 89 bitri ⊢ ( ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
91 85 86 90 3bitri ⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
92 77 78 91 3bitri ⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ∧ ( ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) )
93 75 92 bitrdi ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑍 } ) ( 𝐹 ‘ 𝑍 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
94 20 93 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 , 𝑍 } ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
95 3 94 syl5bb ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) )
96 95 anbi2d ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) ) )
97 2 96 syl5bb ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑍 ) ) ) ) )