fliftfun

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (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$
	fliftfun.4	$⊢ x = y \to A = C$
	fliftfun.5	$⊢ x = y \to B = D$
Assertion	fliftfun	$⊢ φ \to (Fun F \leftrightarrow \forall x \in X \forall y \in X (A = C \to B = D))$

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		fliftfun.4	$⊢ x = y \to A = C$
5		fliftfun.5	$⊢ x = y \to B = D$
6		nfv	$⊢ Ⅎ x φ$
7		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ ⟨A, B⟩)$
8	7	nfrn	$⊢ \underline{Ⅎ} x ran (x \in X ⟼ ⟨A, B⟩)$
9	1 8	nfcxfr	$⊢ \underline{Ⅎ} x F$
10	9	nffun	$⊢ Ⅎ x Fun F$
11		fveq2	$⊢ A = C \to F (A) = F (C)$
12		simplr	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to Fun F$
13	1 2 3	fliftel1	$⊢ (φ \land x \in X) \to A F B$
14	13	ad2ant2r	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to A F B$
15		funbrfv	$⊢ Fun F \to (A F B \to F (A) = B)$
16	12 14 15	sylc	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to F (A) = B$
17		simprr	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to y \in X$
18		eqidd	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to C = C$
19		eqidd	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to D = D$
20	4	eqeq2d	$⊢ x = y \to (C = A \leftrightarrow C = C)$
21	5	eqeq2d	$⊢ x = y \to (D = B \leftrightarrow D = D)$
22	20 21	anbi12d	$⊢ x = y \to ((C = A \land D = B) \leftrightarrow (C = C \land D = D))$
23	22	rspcev	$⊢ (y \in X \land (C = C \land D = D)) \to \exists x \in X (C = A \land D = B)$
24	17 18 19 23	syl12anc	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to \exists x \in X (C = A \land D = B)$
25	1 2 3	fliftel	$⊢ φ \to (C F D \leftrightarrow \exists x \in X (C = A \land D = B))$
26	25	ad2antrr	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to (C F D \leftrightarrow \exists x \in X (C = A \land D = B))$
27	24 26	mpbird	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to C F D$
28		funbrfv	$⊢ Fun F \to (C F D \to F (C) = D)$
29	12 27 28	sylc	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to F (C) = D$
30	16 29	eqeq12d	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to (F (A) = F (C) \leftrightarrow B = D)$
31	11 30	syl5ib	$⊢ ((φ \land Fun F) \land (x \in X \land y \in X)) \to (A = C \to B = D)$
32	31	anassrs	$⊢ (((φ \land Fun F) \land x \in X) \land y \in X) \to (A = C \to B = D)$
33	32	ralrimiva	$⊢ ((φ \land Fun F) \land x \in X) \to \forall y \in X (A = C \to B = D)$
34	33	exp31	$⊢ φ \to (Fun F \to (x \in X \to \forall y \in X (A = C \to B = D)))$
35	6 10 34	ralrimd	$⊢ φ \to (Fun F \to \forall x \in X \forall y \in X (A = C \to B = D))$
36	1 2 3	fliftel	$⊢ φ \to (z F u \leftrightarrow \exists x \in X (z = A \land u = B))$
37	1 2 3	fliftel	$⊢ φ \to (z F v \leftrightarrow \exists x \in X (z = A \land v = B))$
38	4	eqeq2d	$⊢ x = y \to (z = A \leftrightarrow z = C)$
39	5	eqeq2d	$⊢ x = y \to (v = B \leftrightarrow v = D)$
40	38 39	anbi12d	$⊢ x = y \to ((z = A \land v = B) \leftrightarrow (z = C \land v = D))$
41	40	cbvrexvw	$⊢ \exists x \in X (z = A \land v = B) \leftrightarrow \exists y \in X (z = C \land v = D)$
42	37 41	bitrdi	$⊢ φ \to (z F v \leftrightarrow \exists y \in X (z = C \land v = D))$
43	36 42	anbi12d	$⊢ φ \to ((z F u \land z F v) \leftrightarrow (\exists x \in X (z = A \land u = B) \land \exists y \in X (z = C \land v = D)))$
44	43	biimpd	$⊢ φ \to ((z F u \land z F v) \to (\exists x \in X (z = A \land u = B) \land \exists y \in X (z = C \land v = D)))$
45		reeanv	$⊢ \exists x \in X \exists y \in X ((z = A \land u = B) \land (z = C \land v = D)) \leftrightarrow (\exists x \in X (z = A \land u = B) \land \exists y \in X (z = C \land v = D))$
46		r19.29	$⊢ (\forall x \in X \forall y \in X (A = C \to B = D) \land \exists x \in X \exists y \in X ((z = A \land u = B) \land (z = C \land v = D))) \to \exists x \in X (\forall y \in X (A = C \to B = D) \land \exists y \in X ((z = A \land u = B) \land (z = C \land v = D)))$
47		r19.29	$⊢ (\forall y \in X (A = C \to B = D) \land \exists y \in X ((z = A \land u = B) \land (z = C \land v = D))) \to \exists y \in X ((A = C \to B = D) \land ((z = A \land u = B) \land (z = C \land v = D)))$
48		eqtr2	$⊢ (z = A \land z = C) \to A = C$
49	48	ad2ant2r	$⊢ ((z = A \land u = B) \land (z = C \land v = D)) \to A = C$
50	49	imim1i	$⊢ (A = C \to B = D) \to (((z = A \land u = B) \land (z = C \land v = D)) \to B = D)$
51	50	imp	$⊢ ((A = C \to B = D) \land ((z = A \land u = B) \land (z = C \land v = D))) \to B = D$
52		simprlr	$⊢ ((A = C \to B = D) \land ((z = A \land u = B) \land (z = C \land v = D))) \to u = B$
53		simprrr	$⊢ ((A = C \to B = D) \land ((z = A \land u = B) \land (z = C \land v = D))) \to v = D$
54	51 52 53	3eqtr4d	$⊢ ((A = C \to B = D) \land ((z = A \land u = B) \land (z = C \land v = D))) \to u = v$
55	54	rexlimivw	$⊢ \exists y \in X ((A = C \to B = D) \land ((z = A \land u = B) \land (z = C \land v = D))) \to u = v$
56	47 55	syl	$⊢ (\forall y \in X (A = C \to B = D) \land \exists y \in X ((z = A \land u = B) \land (z = C \land v = D))) \to u = v$
57	56	rexlimivw	$⊢ \exists x \in X (\forall y \in X (A = C \to B = D) \land \exists y \in X ((z = A \land u = B) \land (z = C \land v = D))) \to u = v$
58	46 57	syl	$⊢ (\forall x \in X \forall y \in X (A = C \to B = D) \land \exists x \in X \exists y \in X ((z = A \land u = B) \land (z = C \land v = D))) \to u = v$
59	58	ex	$⊢ \forall x \in X \forall y \in X (A = C \to B = D) \to (\exists x \in X \exists y \in X ((z = A \land u = B) \land (z = C \land v = D)) \to u = v)$
60	45 59	syl5bir	$⊢ \forall x \in X \forall y \in X (A = C \to B = D) \to ((\exists x \in X (z = A \land u = B) \land \exists y \in X (z = C \land v = D)) \to u = v)$
61	44 60	syl9	$⊢ φ \to (\forall x \in X \forall y \in X (A = C \to B = D) \to ((z F u \land z F v) \to u = v))$
62	61	alrimdv	$⊢ φ \to (\forall x \in X \forall y \in X (A = C \to B = D) \to \forall v ((z F u \land z F v) \to u = v))$
63	62	alrimdv	$⊢ φ \to (\forall x \in X \forall y \in X (A = C \to B = D) \to \forall u \forall v ((z F u \land z F v) \to u = v))$
64	63	alrimdv	$⊢ φ \to (\forall x \in X \forall y \in X (A = C \to B = D) \to \forall z \forall u \forall v ((z F u \land z F v) \to u = v))$
65	1 2 3	fliftrel	$⊢ φ \to F \subseteq R \times S$
66		relxp	$⊢ Rel (R \times S)$
67		relss	$⊢ F \subseteq R \times S \to (Rel (R \times S) \to Rel F)$
68	65 66 67	mpisyl	$⊢ φ \to Rel F$
69		dffun2	$⊢ Fun F \leftrightarrow (Rel F \land \forall z \forall u \forall v ((z F u \land z F v) \to u = v))$
70	69	baib	$⊢ Rel F \to (Fun F \leftrightarrow \forall z \forall u \forall v ((z F u \land z F v) \to u = v))$
71	68 70	syl	$⊢ φ \to (Fun F \leftrightarrow \forall z \forall u \forall v ((z F u \land z F v) \to u = v))$
72	64 71	sylibrd	$⊢ φ \to (\forall x \in X \forall y \in X (A = C \to B = D) \to Fun F)$
73	35 72	impbid	$⊢ φ \to (Fun F \leftrightarrow \forall x \in X \forall y \in X (A = C \to B = D))$

Metamath Proof Explorer

Theorem fliftfun

Proof