Metamath Proof Explorer

Theorem dff13

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of Monk1 p. 43. (Contributed by NM, 29-Oct-1996)

Ref Expression
Assertion dff13 ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dff12 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑧 ∃* 𝑥 𝑥 𝐹 𝑧 ) )
2 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑧 ∈ V
5 3 4 breldm ⊢ ( 𝑥 𝐹 𝑧 → 𝑥 ∈ dom 𝐹 )
6 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
7 6 eleq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
8 5 7 syl5ib ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑧 → 𝑥 ∈ 𝐴 ) )
9 vex ⊢ 𝑦 ∈ V
10 9 4 breldm ⊢ ( 𝑦 𝐹 𝑧 → 𝑦 ∈ dom 𝐹 )
11 6 eleq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴 ) )
12 10 11 syl5ib ⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 𝐹 𝑧 → 𝑦 ∈ 𝐴 ) )
13 8 12 anim12d ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) )
14 13 pm4.71rd ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) ) ) )
15 eqcom ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑧 )
16 fnbrfvb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑧 ↔ 𝑥 𝐹 𝑧 ) )
17 15 16 syl5bb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑧 ) )
18 eqcom ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = 𝑧 )
19 fnbrfvb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑧 ↔ 𝑦 𝐹 𝑧 ) )
20 18 19 syl5bb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 = ( 𝐹 ‘ 𝑦 ) ↔ 𝑦 𝐹 𝑧 ) )
21 17 20 bi2anan9 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) ) )
22 21 anandis ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) ) )
23 22 pm5.32da ⊢ ( 𝐹 Fn 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) ) ) )
24 14 23 bitr4d ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) ) )
25 24 imbi1d ⊢ ( 𝐹 Fn 𝐴 → ( ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) ) )
26 impexp ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
27 25 26 syl6bb ⊢ ( 𝐹 Fn 𝐴 → ( ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) ) )
28 27 albidv ⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑧 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) ) )
29 19.21v ⊢ ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑧 ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
30 19.23v ⊢ ( ∀ 𝑧 ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
31 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
32 31 eqvinc ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
33 32 imbi1i ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
34 30 33 bitr4i ⊢ ( ∀ 𝑧 ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
35 34 imbi2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑧 ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
36 29 35 bitri ⊢ ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
37 28 36 syl6bb ⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑧 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
38 37 2albidv ⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
39 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐹 𝑧 ↔ 𝑦 𝐹 𝑧 ) )
40 39 mo4 ⊢ ( ∃* 𝑥 𝑥 𝐹 𝑧 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) )
41 40 albii ⊢ ( ∀ 𝑧 ∃* 𝑥 𝑥 𝐹 𝑧 ↔ ∀ 𝑧 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) )
42 alrot3 ⊢ ( ∀ 𝑧 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) )
43 41 42 bitri ⊢ ( ∀ 𝑧 ∃* 𝑥 𝑥 𝐹 𝑧 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐹 𝑧 ∧ 𝑦 𝐹 𝑧 ) → 𝑥 = 𝑦 ) )
44 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
45 38 43 44 3bitr4g ⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑧 ∃* 𝑥 𝑥 𝐹 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
46 2 45 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑧 ∃* 𝑥 𝑥 𝐹 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
47 46 pm5.32i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑧 ∃* 𝑥 𝑥 𝐹 𝑧 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
48 1 47 bitri ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )