xpf1o

Description: Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Hypotheses	xpf1o.1	$⊢ φ \to (x \in A ⟼ X) : A \underset{1-1 onto}{⟶} B$
	xpf1o.2	$⊢ φ \to (y \in C ⟼ Y) : C \underset{1-1 onto}{⟶} D$
Assertion	xpf1o	$⊢ φ \to (x \in A, y \in C ⟼ ⟨X, Y⟩) : A \times C \underset{1-1 onto}{⟶} B \times D$

Proof

Step	Hyp	Ref	Expression
1		xpf1o.1	$⊢ φ \to (x \in A ⟼ X) : A \underset{1-1 onto}{⟶} B$
2		xpf1o.2	$⊢ φ \to (y \in C ⟼ Y) : C \underset{1-1 onto}{⟶} D$
3		xp1st	$⊢ u \in (A \times C) \to 1^{st} (u) \in A$
4	3	adantl	$⊢ (φ \land u \in (A \times C)) \to 1^{st} (u) \in A$
5		eqid	$⊢ (x \in A ⟼ X) = (x \in A ⟼ X)$
6	5	f1ompt	$⊢ (x \in A ⟼ X) : A \underset{1-1 onto}{⟶} B \leftrightarrow (\forall x \in A X \in B \land \forall z \in B \exists! x \in A z = X)$
7	1 6	sylib	$⊢ φ \to (\forall x \in A X \in B \land \forall z \in B \exists! x \in A z = X)$
8	7	simpld	$⊢ φ \to \forall x \in A X \in B$
9	8	adantr	$⊢ (φ \land u \in (A \times C)) \to \forall x \in A X \in B$
10		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ 1^{st} (u) / x ⦌ X$
11	10	nfel1	$⊢ Ⅎ x ⦋ 1^{st} (u) / x ⦌ X \in B$
12		csbeq1a	$⊢ x = 1^{st} (u) \to X = ⦋ 1^{st} (u) / x ⦌ X$
13	12	eleq1d	$⊢ x = 1^{st} (u) \to (X \in B \leftrightarrow ⦋ 1^{st} (u) / x ⦌ X \in B)$
14	11 13	rspc	$⊢ 1^{st} (u) \in A \to (\forall x \in A X \in B \to ⦋ 1^{st} (u) / x ⦌ X \in B)$
15	4 9 14	sylc	$⊢ (φ \land u \in (A \times C)) \to ⦋ 1^{st} (u) / x ⦌ X \in B$
16		xp2nd	$⊢ u \in (A \times C) \to 2^{nd} (u) \in C$
17	16	adantl	$⊢ (φ \land u \in (A \times C)) \to 2^{nd} (u) \in C$
18		eqid	$⊢ (y \in C ⟼ Y) = (y \in C ⟼ Y)$
19	18	f1ompt	$⊢ (y \in C ⟼ Y) : C \underset{1-1 onto}{⟶} D \leftrightarrow (\forall y \in C Y \in D \land \forall w \in D \exists! y \in C w = Y)$
20	2 19	sylib	$⊢ φ \to (\forall y \in C Y \in D \land \forall w \in D \exists! y \in C w = Y)$
21	20	simpld	$⊢ φ \to \forall y \in C Y \in D$
22	21	adantr	$⊢ (φ \land u \in (A \times C)) \to \forall y \in C Y \in D$
23		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ 2^{nd} (u) / y ⦌ Y$
24	23	nfel1	$⊢ Ⅎ y ⦋ 2^{nd} (u) / y ⦌ Y \in D$
25		csbeq1a	$⊢ y = 2^{nd} (u) \to Y = ⦋ 2^{nd} (u) / y ⦌ Y$
26	25	eleq1d	$⊢ y = 2^{nd} (u) \to (Y \in D \leftrightarrow ⦋ 2^{nd} (u) / y ⦌ Y \in D)$
27	24 26	rspc	$⊢ 2^{nd} (u) \in C \to (\forall y \in C Y \in D \to ⦋ 2^{nd} (u) / y ⦌ Y \in D)$
28	17 22 27	sylc	$⊢ (φ \land u \in (A \times C)) \to ⦋ 2^{nd} (u) / y ⦌ Y \in D$
29	15 28	opelxpd	$⊢ (φ \land u \in (A \times C)) \to ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \in (B \times D)$
30	29	ralrimiva	$⊢ φ \to \forall u \in (A \times C) ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \in (B \times D)$
31	7	simprd	$⊢ φ \to \forall z \in B \exists! x \in A z = X$
32	31	r19.21bi	$⊢ (φ \land z \in B) \to \exists! x \in A z = X$
33		reu6	$⊢ \exists! x \in A z = X \leftrightarrow \exists s \in A \forall x \in A (z = X \leftrightarrow x = s)$
34	32 33	sylib	$⊢ (φ \land z \in B) \to \exists s \in A \forall x \in A (z = X \leftrightarrow x = s)$
35	20	simprd	$⊢ φ \to \forall w \in D \exists! y \in C w = Y$
36	35	r19.21bi	$⊢ (φ \land w \in D) \to \exists! y \in C w = Y$
37		reu6	$⊢ \exists! y \in C w = Y \leftrightarrow \exists t \in C \forall y \in C (w = Y \leftrightarrow y = t)$
38	36 37	sylib	$⊢ (φ \land w \in D) \to \exists t \in C \forall y \in C (w = Y \leftrightarrow y = t)$
39	34 38	anim12dan	$⊢ (φ \land (z \in B \land w \in D)) \to (\exists s \in A \forall x \in A (z = X \leftrightarrow x = s) \land \exists t \in C \forall y \in C (w = Y \leftrightarrow y = t))$
40		reeanv	$⊢ \exists s \in A \exists t \in C (\forall x \in A (z = X \leftrightarrow x = s) \land \forall y \in C (w = Y \leftrightarrow y = t)) \leftrightarrow (\exists s \in A \forall x \in A (z = X \leftrightarrow x = s) \land \exists t \in C \forall y \in C (w = Y \leftrightarrow y = t))$
41		pm4.38	$⊢ ((z = X \leftrightarrow x = s) \land (w = Y \leftrightarrow y = t)) \to ((z = X \land w = Y) \leftrightarrow (x = s \land y = t))$
42	41	ex	$⊢ (z = X \leftrightarrow x = s) \to ((w = Y \leftrightarrow y = t) \to ((z = X \land w = Y) \leftrightarrow (x = s \land y = t)))$
43	42	ralimdv	$⊢ (z = X \leftrightarrow x = s) \to (\forall y \in C (w = Y \leftrightarrow y = t) \to \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t)))$
44	43	com12	$⊢ \forall y \in C (w = Y \leftrightarrow y = t) \to ((z = X \leftrightarrow x = s) \to \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t)))$
45	44	ralimdv	$⊢ \forall y \in C (w = Y \leftrightarrow y = t) \to (\forall x \in A (z = X \leftrightarrow x = s) \to \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t)))$
46	45	impcom	$⊢ (\forall x \in A (z = X \leftrightarrow x = s) \land \forall y \in C (w = Y \leftrightarrow y = t)) \to \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t))$
47	46	reximi	$⊢ \exists t \in C (\forall x \in A (z = X \leftrightarrow x = s) \land \forall y \in C (w = Y \leftrightarrow y = t)) \to \exists t \in C \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t))$
48	47	reximi	$⊢ \exists s \in A \exists t \in C (\forall x \in A (z = X \leftrightarrow x = s) \land \forall y \in C (w = Y \leftrightarrow y = t)) \to \exists s \in A \exists t \in C \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t))$
49	40 48	sylbir	$⊢ (\exists s \in A \forall x \in A (z = X \leftrightarrow x = s) \land \exists t \in C \forall y \in C (w = Y \leftrightarrow y = t)) \to \exists s \in A \exists t \in C \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t))$
50	39 49	syl	$⊢ (φ \land (z \in B \land w \in D)) \to \exists s \in A \exists t \in C \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t))$
51		vex	$⊢ s \in V$
52		vex	$⊢ t \in V$
53	51 52	op1std	$⊢ u = ⟨s, t⟩ \to 1^{st} (u) = s$
54	53	csbeq1d	$⊢ u = ⟨s, t⟩ \to ⦋ 1^{st} (u) / x ⦌ X = ⦋ s / x ⦌ X$
55	54	eqeq2d	$⊢ u = ⟨s, t⟩ \to (z = ⦋ 1^{st} (u) / x ⦌ X \leftrightarrow z = ⦋ s / x ⦌ X)$
56	51 52	op2ndd	$⊢ u = ⟨s, t⟩ \to 2^{nd} (u) = t$
57	56	csbeq1d	$⊢ u = ⟨s, t⟩ \to ⦋ 2^{nd} (u) / y ⦌ Y = ⦋ t / y ⦌ Y$
58	57	eqeq2d	$⊢ u = ⟨s, t⟩ \to (w = ⦋ 2^{nd} (u) / y ⦌ Y \leftrightarrow w = ⦋ t / y ⦌ Y)$
59	55 58	anbi12d	$⊢ u = ⟨s, t⟩ \to ((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow (z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y))$
60		eqeq1	$⊢ u = ⟨s, t⟩ \to (u = v \leftrightarrow ⟨s, t⟩ = v)$
61	59 60	bibi12d	$⊢ u = ⟨s, t⟩ \to (((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow u = v) \leftrightarrow ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v))$
62	61	ralxp	$⊢ \forall u \in (A \times C) ((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow u = v) \leftrightarrow \forall s \in A \forall t \in C ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v)$
63		nfv	$⊢ Ⅎ s \forall y \in C ((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v)$
64		nfcv	$⊢ \underline{Ⅎ} x C$
65		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ X$
66	65	nfeq2	$⊢ Ⅎ x z = ⦋ s / x ⦌ X$
67		nfv	$⊢ Ⅎ x w = ⦋ t / y ⦌ Y$
68	66 67	nfan	$⊢ Ⅎ x (z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y)$
69		nfv	$⊢ Ⅎ x ⟨s, t⟩ = v$
70	68 69	nfbi	$⊢ Ⅎ x ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v)$
71	64 70	nfralw	$⊢ Ⅎ x \forall t \in C ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v)$
72		nfv	$⊢ Ⅎ t ((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v)$
73		nfv	$⊢ Ⅎ y z = X$
74		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ t / y ⦌ Y$
75	74	nfeq2	$⊢ Ⅎ y w = ⦋ t / y ⦌ Y$
76	73 75	nfan	$⊢ Ⅎ y (z = X \land w = ⦋ t / y ⦌ Y)$
77		nfv	$⊢ Ⅎ y ⟨x, t⟩ = v$
78	76 77	nfbi	$⊢ Ⅎ y ((z = X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨x, t⟩ = v)$
79		csbeq1a	$⊢ y = t \to Y = ⦋ t / y ⦌ Y$
80	79	eqeq2d	$⊢ y = t \to (w = Y \leftrightarrow w = ⦋ t / y ⦌ Y)$
81	80	anbi2d	$⊢ y = t \to ((z = X \land w = Y) \leftrightarrow (z = X \land w = ⦋ t / y ⦌ Y))$
82		opeq2	$⊢ y = t \to ⟨x, y⟩ = ⟨x, t⟩$
83	82	eqeq1d	$⊢ y = t \to (⟨x, y⟩ = v \leftrightarrow ⟨x, t⟩ = v)$
84	81 83	bibi12d	$⊢ y = t \to (((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v) \leftrightarrow ((z = X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨x, t⟩ = v))$
85	72 78 84	cbvralw	$⊢ \forall y \in C ((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v) \leftrightarrow \forall t \in C ((z = X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨x, t⟩ = v)$
86		csbeq1a	$⊢ x = s \to X = ⦋ s / x ⦌ X$
87	86	eqeq2d	$⊢ x = s \to (z = X \leftrightarrow z = ⦋ s / x ⦌ X)$
88	87	anbi1d	$⊢ x = s \to ((z = X \land w = ⦋ t / y ⦌ Y) \leftrightarrow (z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y))$
89		opeq1	$⊢ x = s \to ⟨x, t⟩ = ⟨s, t⟩$
90	89	eqeq1d	$⊢ x = s \to (⟨x, t⟩ = v \leftrightarrow ⟨s, t⟩ = v)$
91	88 90	bibi12d	$⊢ x = s \to (((z = X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨x, t⟩ = v) \leftrightarrow ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v))$
92	91	ralbidv	$⊢ x = s \to (\forall t \in C ((z = X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨x, t⟩ = v) \leftrightarrow \forall t \in C ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v))$
93	85 92	syl5bb	$⊢ x = s \to (\forall y \in C ((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v) \leftrightarrow \forall t \in C ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v))$
94	63 71 93	cbvralw	$⊢ \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v) \leftrightarrow \forall s \in A \forall t \in C ((z = ⦋ s / x ⦌ X \land w = ⦋ t / y ⦌ Y) \leftrightarrow ⟨s, t⟩ = v)$
95	62 94	bitr4i	$⊢ \forall u \in (A \times C) ((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow u = v) \leftrightarrow \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v)$
96		eqeq2	$⊢ v = ⟨s, t⟩ \to (⟨x, y⟩ = v \leftrightarrow ⟨x, y⟩ = ⟨s, t⟩)$
97		vex	$⊢ x \in V$
98		vex	$⊢ y \in V$
99	97 98	opth	$⊢ ⟨x, y⟩ = ⟨s, t⟩ \leftrightarrow (x = s \land y = t)$
100	96 99	syl6bb	$⊢ v = ⟨s, t⟩ \to (⟨x, y⟩ = v \leftrightarrow (x = s \land y = t))$
101	100	bibi2d	$⊢ v = ⟨s, t⟩ \to (((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v) \leftrightarrow ((z = X \land w = Y) \leftrightarrow (x = s \land y = t)))$
102	101	2ralbidv	$⊢ v = ⟨s, t⟩ \to (\forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow ⟨x, y⟩ = v) \leftrightarrow \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t)))$
103	95 102	syl5bb	$⊢ v = ⟨s, t⟩ \to (\forall u \in (A \times C) ((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow u = v) \leftrightarrow \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t)))$
104	103	rexxp	$⊢ \exists v \in (A \times C) \forall u \in (A \times C) ((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow u = v) \leftrightarrow \exists s \in A \exists t \in C \forall x \in A \forall y \in C ((z = X \land w = Y) \leftrightarrow (x = s \land y = t))$
105	50 104	sylibr	$⊢ (φ \land (z \in B \land w \in D)) \to \exists v \in (A \times C) \forall u \in (A \times C) ((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow u = v)$
106		reu6	$⊢ \exists! u \in (A \times C) (z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow \exists v \in (A \times C) \forall u \in (A \times C) ((z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y) \leftrightarrow u = v)$
107	105 106	sylibr	$⊢ (φ \land (z \in B \land w \in D)) \to \exists! u \in (A \times C) (z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y)$
108	107	ralrimivva	$⊢ φ \to \forall z \in B \forall w \in D \exists! u \in (A \times C) (z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y)$
109		eqeq1	$⊢ v = ⟨z, w⟩ \to (v = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \leftrightarrow ⟨z, w⟩ = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩)$
110		vex	$⊢ z \in V$
111		vex	$⊢ w \in V$
112	110 111	opth	$⊢ ⟨z, w⟩ = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \leftrightarrow (z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y)$
113	109 112	syl6bb	$⊢ v = ⟨z, w⟩ \to (v = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \leftrightarrow (z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y))$
114	113	reubidv	$⊢ v = ⟨z, w⟩ \to (\exists! u \in (A \times C) v = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \leftrightarrow \exists! u \in (A \times C) (z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y))$
115	114	ralxp	$⊢ \forall v \in (B \times D) \exists! u \in (A \times C) v = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \leftrightarrow \forall z \in B \forall w \in D \exists! u \in (A \times C) (z = ⦋ 1^{st} (u) / x ⦌ X \land w = ⦋ 2^{nd} (u) / y ⦌ Y)$
116	108 115	sylibr	$⊢ φ \to \forall v \in (B \times D) \exists! u \in (A \times C) v = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩$
117		nfcv	$⊢ \underline{Ⅎ} z ⟨X, Y⟩$
118		nfcv	$⊢ \underline{Ⅎ} w ⟨X, Y⟩$
119		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ z / x ⦌ X$
120		nfcv	$⊢ \underline{Ⅎ} x ⦋ w / y ⦌ Y$
121	119 120	nfop	$⊢ \underline{Ⅎ} x ⟨⦋ z / x ⦌ X, ⦋ w / y ⦌ Y⟩$
122		nfcv	$⊢ \underline{Ⅎ} y ⦋ z / x ⦌ X$
123		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ w / y ⦌ Y$
124	122 123	nfop	$⊢ \underline{Ⅎ} y ⟨⦋ z / x ⦌ X, ⦋ w / y ⦌ Y⟩$
125		csbeq1a	$⊢ x = z \to X = ⦋ z / x ⦌ X$
126		csbeq1a	$⊢ y = w \to Y = ⦋ w / y ⦌ Y$
127		opeq12	$⊢ (X = ⦋ z / x ⦌ X \land Y = ⦋ w / y ⦌ Y) \to ⟨X, Y⟩ = ⟨⦋ z / x ⦌ X, ⦋ w / y ⦌ Y⟩$
128	125 126 127	syl2an	$⊢ (x = z \land y = w) \to ⟨X, Y⟩ = ⟨⦋ z / x ⦌ X, ⦋ w / y ⦌ Y⟩$
129	117 118 121 124 128	cbvmpo	$⊢ (x \in A, y \in C ⟼ ⟨X, Y⟩) = (z \in A, w \in C ⟼ ⟨⦋ z / x ⦌ X, ⦋ w / y ⦌ Y⟩)$
130	110 111	op1std	$⊢ u = ⟨z, w⟩ \to 1^{st} (u) = z$
131	130	csbeq1d	$⊢ u = ⟨z, w⟩ \to ⦋ 1^{st} (u) / x ⦌ X = ⦋ z / x ⦌ X$
132	110 111	op2ndd	$⊢ u = ⟨z, w⟩ \to 2^{nd} (u) = w$
133	132	csbeq1d	$⊢ u = ⟨z, w⟩ \to ⦋ 2^{nd} (u) / y ⦌ Y = ⦋ w / y ⦌ Y$
134	131 133	opeq12d	$⊢ u = ⟨z, w⟩ \to ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ = ⟨⦋ z / x ⦌ X, ⦋ w / y ⦌ Y⟩$
135	134	mpompt	$⊢ (u \in (A \times C) ⟼ ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩) = (z \in A, w \in C ⟼ ⟨⦋ z / x ⦌ X, ⦋ w / y ⦌ Y⟩)$
136	129 135	eqtr4i	$⊢ (x \in A, y \in C ⟼ ⟨X, Y⟩) = (u \in (A \times C) ⟼ ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩)$
137	136	f1ompt	$⊢ (x \in A, y \in C ⟼ ⟨X, Y⟩) : A \times C \underset{1-1 onto}{⟶} B \times D \leftrightarrow (\forall u \in (A \times C) ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩ \in (B \times D) \land \forall v \in (B \times D) \exists! u \in (A \times C) v = ⟨⦋ 1^{st} (u) / x ⦌ X, ⦋ 2^{nd} (u) / y ⦌ Y⟩)$
138	30 116 137	sylanbrc	$⊢ φ \to (x \in A, y \in C ⟼ ⟨X, Y⟩) : A \times C \underset{1-1 onto}{⟶} B \times D$

Metamath Proof Explorer

Theorem xpf1o

Proof