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 bitrid ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( 𝑧 = ( 𝐹𝑥 ) ↔ 𝑥 𝐹 𝑧 ) )
18 eqcom ( 𝑧 = ( 𝐹𝑦 ) ↔ ( 𝐹𝑦 ) = 𝑧 )
19 fnbrfvb ( ( 𝐹 Fn 𝐴𝑦𝐴 ) → ( ( 𝐹𝑦 ) = 𝑧𝑦 𝐹 𝑧 ) )
20 18 19 bitrid ( ( 𝐹 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 bitrdi ( 𝐹 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 bitrdi ( 𝐹 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𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )