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	syl6bb	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ 𝑦 ∈ 𝐴 ) )
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→ 𝐵 )