Metamath Proof Explorer

Theorem f12dfv

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

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

Proof

Step Hyp Ref Expression
1 f12dfv.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 8 13 ralprg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) )
15 14 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) )
16 1 difeq1i ⊢ ( 𝐴 ∖ { 𝑋 } ) = ( { 𝑋 , 𝑌 } ∖ { 𝑋 } )
17 difprsn1 ⊢ ( 𝑋 ≠ 𝑌 → ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) = { 𝑌 } )
18 16 17 eqtrid ⊢ ( 𝑋 ≠ 𝑌 → ( 𝐴 ∖ { 𝑋 } ) = { 𝑌 } )
19 18 adantl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ∖ { 𝑋 } ) = { 𝑌 } )
20 19 raleqdv ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑌 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
21 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
22 21 neeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
23 22 ralsng ⊢ ( 𝑌 ∈ 𝑉 → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
24 23 adantl ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
25 24 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
26 20 25 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
27 1 difeq1i ⊢ ( 𝐴 ∖ { 𝑌 } ) = ( { 𝑋 , 𝑌 } ∖ { 𝑌 } )
28 difprsn2 ⊢ ( 𝑋 ≠ 𝑌 → ( { 𝑋 , 𝑌 } ∖ { 𝑌 } ) = { 𝑋 } )
29 27 28 eqtrid ⊢ ( 𝑋 ≠ 𝑌 → ( 𝐴 ∖ { 𝑌 } ) = { 𝑋 } )
30 29 adantl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ∖ { 𝑌 } ) = { 𝑋 } )
31 30 raleqdv ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑋 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
32 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
33 32 neeq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
34 33 ralsng ⊢ ( 𝑋 ∈ 𝑈 → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
35 34 adantr ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
36 35 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
37 31 36 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
38 26 37 anbi12d ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) ) )
39 necom ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) )
40 39 biimpi ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) → ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) )
41 40 pm4.71i ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
42 38 41 bitr4di ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑌 } ) ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
43 15 42 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
44 3 43 syl5bb ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
45 44 anbi2d ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
46 2 45 syl5bb ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )