fliftf

Description: The domain and range of the function F . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
	flift.2	$⊢ (φ \land x \in X) \to A \in R$
	flift.3	$⊢ (φ \land x \in X) \to B \in S$
Assertion	fliftf	$⊢ φ \to (Fun F \leftrightarrow F : ran (x \in X ⟼ A) ⟶ S)$

Proof

Step	Hyp	Ref	Expression
1		flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
2		flift.2	$⊢ (φ \land x \in X) \to A \in R$
3		flift.3	$⊢ (φ \land x \in X) \to B \in S$
4		simpr	$⊢ (φ \land Fun F) \to Fun F$
5	1 2 3	fliftel	$⊢ φ \to (y F z \leftrightarrow \exists x \in X (y = A \land z = B))$
6	5	exbidv	$⊢ φ \to (\exists z y F z \leftrightarrow \exists z \exists x \in X (y = A \land z = B))$
7	6	adantr	$⊢ (φ \land Fun F) \to (\exists z y F z \leftrightarrow \exists z \exists x \in X (y = A \land z = B))$
8		rexcom4	$⊢ \exists x \in X \exists z (y = A \land z = B) \leftrightarrow \exists z \exists x \in X (y = A \land z = B)$
9		elisset	$⊢ B \in S \to \exists z z = B$
10	3 9	syl	$⊢ (φ \land x \in X) \to \exists z z = B$
11	10	biantrud	$⊢ (φ \land x \in X) \to (y = A \leftrightarrow (y = A \land \exists z z = B))$
12		19.42v	$⊢ \exists z (y = A \land z = B) \leftrightarrow (y = A \land \exists z z = B)$
13	11 12	syl6rbbr	$⊢ (φ \land x \in X) \to (\exists z (y = A \land z = B) \leftrightarrow y = A)$
14	13	rexbidva	$⊢ φ \to (\exists x \in X \exists z (y = A \land z = B) \leftrightarrow \exists x \in X y = A)$
15	14	adantr	$⊢ (φ \land Fun F) \to (\exists x \in X \exists z (y = A \land z = B) \leftrightarrow \exists x \in X y = A)$
16	8 15	bitr3id	$⊢ (φ \land Fun F) \to (\exists z \exists x \in X (y = A \land z = B) \leftrightarrow \exists x \in X y = A)$
17	7 16	bitrd	$⊢ (φ \land Fun F) \to (\exists z y F z \leftrightarrow \exists x \in X y = A)$
18	17	abbidv	$⊢ (φ \land Fun F) \to \{y \| \exists z y F z\} = \{y \| \exists x \in X y = A\}$
19		df-dm	$⊢ dom F = \{y \| \exists z y F z\}$
20		eqid	$⊢ (x \in X ⟼ A) = (x \in X ⟼ A)$
21	20	rnmpt	$⊢ ran (x \in X ⟼ A) = \{y \| \exists x \in X y = A\}$
22	18 19 21	3eqtr4g	$⊢ (φ \land Fun F) \to dom F = ran (x \in X ⟼ A)$
23		df-fn	$⊢ F Fn ran (x \in X ⟼ A) \leftrightarrow (Fun F \land dom F = ran (x \in X ⟼ A))$
24	4 22 23	sylanbrc	$⊢ (φ \land Fun F) \to F Fn ran (x \in X ⟼ A)$
25	1 2 3	fliftrel	$⊢ φ \to F \subseteq R \times S$
26	25	adantr	$⊢ (φ \land Fun F) \to F \subseteq R \times S$
27		rnss	$⊢ F \subseteq R \times S \to ran F \subseteq ran (R \times S)$
28	26 27	syl	$⊢ (φ \land Fun F) \to ran F \subseteq ran (R \times S)$
29		rnxpss	$⊢ ran (R \times S) \subseteq S$
30	28 29	sstrdi	$⊢ (φ \land Fun F) \to ran F \subseteq S$
31		df-f	$⊢ F : ran (x \in X ⟼ A) ⟶ S \leftrightarrow (F Fn ran (x \in X ⟼ A) \land ran F \subseteq S)$
32	24 30 31	sylanbrc	$⊢ (φ \land Fun F) \to F : ran (x \in X ⟼ A) ⟶ S$
33	32	ex	$⊢ φ \to (Fun F \to F : ran (x \in X ⟼ A) ⟶ S)$
34		ffun	$⊢ F : ran (x \in X ⟼ A) ⟶ S \to Fun F$
35	33 34	impbid1	$⊢ φ \to (Fun F \leftrightarrow F : ran (x \in X ⟼ A) ⟶ S)$

Metamath Proof Explorer

Theorem fliftf

Proof