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𝐵 )