This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dom2lem

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004)

Ref Expression
Hypotheses dom2d.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
dom2d.2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) )
Assertion dom2lem ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 dom2d.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
2 dom2d.2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) )
3 1 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
4 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
5 4 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
6 3 5 sylib ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
7 1 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
8 4 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
9 8 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
10 7 9 mpdan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
11 10 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
12 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 )
13 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 )
14 13 nfeq1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷
15 12 14 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 )
16 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
17 16 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
18 17 imbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 ) ) )
19 16 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) )
20 anidm ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ 𝑦 ∈ 𝐴 )
21 19 20 bitrdi ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ 𝑦 ∈ 𝐴 ) )
22 21 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
23 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
24 23 adantr ⊢ ( ( 𝑥 = 𝑦 ∧ ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
25 2 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) )
26 25 biimparc ⊢ ( ( 𝑥 = 𝑦 ∧ ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ) → 𝐶 = 𝐷 )
27 24 26 eqeq12d ⊢ ( ( 𝑥 = 𝑦 ∧ ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 ) )
28 27 ex ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 ) ) )
29 22 28 sylbird ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 ) ) )
30 29 pm5.74d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 ) ) )
31 18 30 bitrd ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 ) ) )
32 15 31 10 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 )
33 32 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐷 )
34 11 33 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ 𝐶 = 𝐷 ) )
35 25 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) )
36 34 35 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
37 36 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
38 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
39 nfcv ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
40 38 39 dff13f ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
41 6 37 40 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1→ 𝐵 )