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	$⊢ φ \to (x \in A \to C \in B)$
	dom2d.2	$⊢ φ \to ((x \in A \land y \in A) \to (C = D \leftrightarrow x = y))$
Assertion	dom2lem	$⊢ φ \to (x \in A ⟼ C) : A \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		dom2d.1	$⊢ φ \to (x \in A \to C \in B)$
2		dom2d.2	$⊢ φ \to ((x \in A \land y \in A) \to (C = D \leftrightarrow x = y))$
3	1	ralrimiv	$⊢ φ \to \forall x \in A C \in B$
4		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
5	4	fmpt	$⊢ \forall x \in A C \in B \leftrightarrow (x \in A ⟼ C) : A ⟶ B$
6	3 5	sylib	$⊢ φ \to (x \in A ⟼ C) : A ⟶ B$
7	1	imp	$⊢ (φ \land x \in A) \to C \in B$
8	4	fvmpt2	$⊢ (x \in A \land C \in B) \to (x \in A ⟼ C) (x) = C$
9	8	adantll	$⊢ ((φ \land x \in A) \land C \in B) \to (x \in A ⟼ C) (x) = C$
10	7 9	mpdan	$⊢ (φ \land x \in A) \to (x \in A ⟼ C) (x) = C$
11	10	adantrr	$⊢ (φ \land (x \in A \land y \in A)) \to (x \in A ⟼ C) (x) = C$
12		nfv	$⊢ Ⅎ x (φ \land y \in A)$
13		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C) (y)$
14	13	nfeq1	$⊢ Ⅎ x (x \in A ⟼ C) (y) = D$
15	12 14	nfim	$⊢ Ⅎ x ((φ \land y \in A) \to (x \in A ⟼ C) (y) = D)$
16		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
17	16	anbi2d	$⊢ x = y \to ((φ \land x \in A) \leftrightarrow (φ \land y \in A))$
18	17	imbi1d	$⊢ x = y \to (((φ \land x \in A) \to (x \in A ⟼ C) (x) = C) \leftrightarrow ((φ \land y \in A) \to (x \in A ⟼ C) (x) = C))$
19	16	anbi1d	$⊢ x = y \to ((x \in A \land y \in A) \leftrightarrow (y \in A \land y \in A))$
20		anidm	$⊢ (y \in A \land y \in A) \leftrightarrow y \in A$
21	19 20	bitrdi	$⊢ x = y \to ((x \in A \land y \in A) \leftrightarrow y \in A)$
22	21	anbi2d	$⊢ x = y \to ((φ \land (x \in A \land y \in A)) \leftrightarrow (φ \land y \in A))$
23		fveq2	$⊢ x = y \to (x \in A ⟼ C) (x) = (x \in A ⟼ C) (y)$
24	23	adantr	$⊢ (x = y \land (φ \land (x \in A \land y \in A))) \to (x \in A ⟼ C) (x) = (x \in A ⟼ C) (y)$
25	2	imp	$⊢ (φ \land (x \in A \land y \in A)) \to (C = D \leftrightarrow x = y)$
26	25	biimparc	$⊢ (x = y \land (φ \land (x \in A \land y \in A))) \to C = D$
27	24 26	eqeq12d	$⊢ (x = y \land (φ \land (x \in A \land y \in A))) \to ((x \in A ⟼ C) (x) = C \leftrightarrow (x \in A ⟼ C) (y) = D)$
28	27	ex	$⊢ x = y \to ((φ \land (x \in A \land y \in A)) \to ((x \in A ⟼ C) (x) = C \leftrightarrow (x \in A ⟼ C) (y) = D))$
29	22 28	sylbird	$⊢ x = y \to ((φ \land y \in A) \to ((x \in A ⟼ C) (x) = C \leftrightarrow (x \in A ⟼ C) (y) = D))$
30	29	pm5.74d	$⊢ x = y \to (((φ \land y \in A) \to (x \in A ⟼ C) (x) = C) \leftrightarrow ((φ \land y \in A) \to (x \in A ⟼ C) (y) = D))$
31	18 30	bitrd	$⊢ x = y \to (((φ \land x \in A) \to (x \in A ⟼ C) (x) = C) \leftrightarrow ((φ \land y \in A) \to (x \in A ⟼ C) (y) = D))$
32	15 31 10	chvarfv	$⊢ (φ \land y \in A) \to (x \in A ⟼ C) (y) = D$
33	32	adantrl	$⊢ (φ \land (x \in A \land y \in A)) \to (x \in A ⟼ C) (y) = D$
34	11 33	eqeq12d	$⊢ (φ \land (x \in A \land y \in A)) \to ((x \in A ⟼ C) (x) = (x \in A ⟼ C) (y) \leftrightarrow C = D)$
35	25	biimpd	$⊢ (φ \land (x \in A \land y \in A)) \to (C = D \to x = y)$
36	34 35	sylbid	$⊢ (φ \land (x \in A \land y \in A)) \to ((x \in A ⟼ C) (x) = (x \in A ⟼ C) (y) \to x = y)$
37	36	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in A ((x \in A ⟼ C) (x) = (x \in A ⟼ C) (y) \to x = y)$
38		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C)$
39		nfcv	$⊢ \underline{Ⅎ} y (x \in A ⟼ C)$
40	38 39	dff13f	$⊢ (x \in A ⟼ C) : A \underset{1-1}{⟶} B \leftrightarrow ((x \in A ⟼ C) : A ⟶ B \land \forall x \in A \forall y \in A ((x \in A ⟼ C) (x) = (x \in A ⟼ C) (y) \to x = y))$
41	6 37 40	sylanbrc	$⊢ φ \to (x \in A ⟼ C) : A \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem dom2lem

Proof