Metamath Proof Explorer

Theorem dff13f

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

Ref Expression
Hypotheses dff13f.1 ⊢ Ⅎ 𝑥 𝐹
dff13f.2 ⊢ Ⅎ 𝑦 𝐹
Assertion dff13f ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dff13f.1 ⊢ Ⅎ 𝑥 𝐹
2 dff13f.2 ⊢ Ⅎ 𝑦 𝐹
3 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) → 𝑤 = 𝑣 ) ) )
4 nfcv ⊢ Ⅎ 𝑦 𝑤
5 2 4 nffv ⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑤 )
6 nfcv ⊢ Ⅎ 𝑦 𝑣
7 2 6 nffv ⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑣 )
8 5 7 nfeq ⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 )
9 nfv ⊢ Ⅎ 𝑦 𝑤 = 𝑣
10 8 9 nfim ⊢ Ⅎ 𝑦 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) → 𝑤 = 𝑣 )
11 nfv ⊢ Ⅎ 𝑣 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 )
12 fveq2 ⊢ ( 𝑣 = 𝑦 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑦 ) )
13 12 eqeq2d ⊢ ( 𝑣 = 𝑦 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ) )
14 equequ2 ⊢ ( 𝑣 = 𝑦 → ( 𝑤 = 𝑣 ↔ 𝑤 = 𝑦 ) )
15 13 14 imbi12d ⊢ ( 𝑣 = 𝑦 → ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) → 𝑤 = 𝑣 ) ↔ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 ) ) )
16 10 11 15 cbvralw ⊢ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) → 𝑤 = 𝑣 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 ) )
17 16 ralbii ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) → 𝑤 = 𝑣 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 ) )
18 nfcv ⊢ Ⅎ 𝑥 𝐴
19 nfcv ⊢ Ⅎ 𝑥 𝑤
20 1 19 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑤 )
21 nfcv ⊢ Ⅎ 𝑥 𝑦
22 1 21 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
23 20 22 nfeq ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 )
24 nfv ⊢ Ⅎ 𝑥 𝑤 = 𝑦
25 23 24 nfim ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 )
26 18 25 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 )
27 nfv ⊢ Ⅎ 𝑤 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 )
28 fveqeq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
29 equequ1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝑦 ↔ 𝑥 = 𝑦 ) )
30 28 29 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
31 30 ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
32 26 27 31 cbvralw ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) → 𝑤 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
33 17 32 bitri ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) → 𝑤 = 𝑣 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
34 33 anbi2i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) → 𝑤 = 𝑣 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
35 3 34 bitri ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )