xpsff1o

Description: The function appearing in xpsval is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o } . (Contributed by Mario Carneiro, 15-Aug-2015)

		Ref	Expression
	Hypothesis	xpsff1o.f	$⊢ F = (x \in A, y \in B ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
	Assertion	xpsff1o	$⊢ F : A \times B \underset{1-1 onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$

Proof

Step	Hyp	Ref	Expression
1		xpsff1o.f	$⊢ F = (x \in A, y \in B ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
2		xpsfrnel2	$⊢ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (x \in A \land y \in B)$
3	2	biimpri	$⊢ (x \in A \land y \in B) \to \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
4	3	rgen2	$⊢ \forall x \in A \forall y \in B \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
5	1	fmpo	$⊢ \forall x \in A \forall y \in B \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow F : A \times B ⟶ \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
6	4 5	mpbi	$⊢ F : A \times B ⟶ \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
7		1st2nd2	$⊢ z \in (A \times B) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
8	7	fveq2d	$⊢ z \in (A \times B) \to F (z) = F (⟨1^{st} (z), 2^{nd} (z)⟩)$
9		df-ov	$⊢ 1^{st} (z) F 2^{nd} (z) = F (⟨1^{st} (z), 2^{nd} (z)⟩)$
10		xp1st	$⊢ z \in (A \times B) \to 1^{st} (z) \in A$
11		xp2nd	$⊢ z \in (A \times B) \to 2^{nd} (z) \in B$
12	1	xpsfval	$⊢ (1^{st} (z) \in A \land 2^{nd} (z) \in B) \to 1^{st} (z) F 2^{nd} (z) = \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\}$
13	10 11 12	syl2anc	$⊢ z \in (A \times B) \to 1^{st} (z) F 2^{nd} (z) = \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\}$
14	9 13	syl5eqr	$⊢ z \in (A \times B) \to F (⟨1^{st} (z), 2^{nd} (z)⟩) = \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\}$
15	8 14	eqtrd	$⊢ z \in (A \times B) \to F (z) = \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\}$
16		1st2nd2	$⊢ w \in (A \times B) \to w = ⟨1^{st} (w), 2^{nd} (w)⟩$
17	16	fveq2d	$⊢ w \in (A \times B) \to F (w) = F (⟨1^{st} (w), 2^{nd} (w)⟩)$
18		df-ov	$⊢ 1^{st} (w) F 2^{nd} (w) = F (⟨1^{st} (w), 2^{nd} (w)⟩)$
19		xp1st	$⊢ w \in (A \times B) \to 1^{st} (w) \in A$
20		xp2nd	$⊢ w \in (A \times B) \to 2^{nd} (w) \in B$
21	1	xpsfval	$⊢ (1^{st} (w) \in A \land 2^{nd} (w) \in B) \to 1^{st} (w) F 2^{nd} (w) = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\}$
22	19 20 21	syl2anc	$⊢ w \in (A \times B) \to 1^{st} (w) F 2^{nd} (w) = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\}$
23	18 22	syl5eqr	$⊢ w \in (A \times B) \to F (⟨1^{st} (w), 2^{nd} (w)⟩) = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\}$
24	17 23	eqtrd	$⊢ w \in (A \times B) \to F (w) = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\}$
25	15 24	eqeqan12d	$⊢ (z \in (A \times B) \land w \in (A \times B)) \to (F (z) = F (w) \leftrightarrow \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\})$
26		fveq1	$⊢ \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} \to \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} (\emptyset) = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} (\emptyset)$
27		fvex	$⊢ 1^{st} (z) \in V$
28		fvpr0o	$⊢ 1^{st} (z) \in V \to \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} (\emptyset) = 1^{st} (z)$
29	27 28	ax-mp	$⊢ \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} (\emptyset) = 1^{st} (z)$
30		fvex	$⊢ 1^{st} (w) \in V$
31		fvpr0o	$⊢ 1^{st} (w) \in V \to \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} (\emptyset) = 1^{st} (w)$
32	30 31	ax-mp	$⊢ \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} (\emptyset) = 1^{st} (w)$
33	26 29 32	3eqtr3g	$⊢ \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} \to 1^{st} (z) = 1^{st} (w)$
34		fveq1	$⊢ \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} \to \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} (1_{𝑜}) = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} (1_{𝑜})$
35		fvex	$⊢ 2^{nd} (z) \in V$
36		fvpr1o	$⊢ 2^{nd} (z) \in V \to \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} (1_{𝑜}) = 2^{nd} (z)$
37	35 36	ax-mp	$⊢ \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} (1_{𝑜}) = 2^{nd} (z)$
38		fvex	$⊢ 2^{nd} (w) \in V$
39		fvpr1o	$⊢ 2^{nd} (w) \in V \to \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} (1_{𝑜}) = 2^{nd} (w)$
40	38 39	ax-mp	$⊢ \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} (1_{𝑜}) = 2^{nd} (w)$
41	34 37 40	3eqtr3g	$⊢ \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} \to 2^{nd} (z) = 2^{nd} (w)$
42	33 41	opeq12d	$⊢ \{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} \to ⟨1^{st} (z), 2^{nd} (z)⟩ = ⟨1^{st} (w), 2^{nd} (w)⟩$
43	7 16	eqeqan12d	$⊢ (z \in (A \times B) \land w \in (A \times B)) \to (z = w \leftrightarrow ⟨1^{st} (z), 2^{nd} (z)⟩ = ⟨1^{st} (w), 2^{nd} (w)⟩)$
44	42 43	syl5ibr	$⊢ (z \in (A \times B) \land w \in (A \times B)) \to (\{⟨\emptyset, 1^{st} (z)⟩, ⟨1_{𝑜}, 2^{nd} (z)⟩\} = \{⟨\emptyset, 1^{st} (w)⟩, ⟨1_{𝑜}, 2^{nd} (w)⟩\} \to z = w)$
45	25 44	sylbid	$⊢ (z \in (A \times B) \land w \in (A \times B)) \to (F (z) = F (w) \to z = w)$
46	45	rgen2	$⊢ \forall z \in (A \times B) \forall w \in (A \times B) (F (z) = F (w) \to z = w)$
47		dff13	$⊢ F : A \times B \underset{1-1}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (F : A \times B ⟶ \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \land \forall z \in (A \times B) \forall w \in (A \times B) (F (z) = F (w) \to z = w))$
48	6 46 47	mpbir2an	$⊢ F : A \times B \underset{1-1}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
49		xpsfrnel	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (z Fn 2_{𝑜} \land z (\emptyset) \in A \land z (1_{𝑜}) \in B)$
50	49	simp2bi	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to z (\emptyset) \in A$
51	49	simp3bi	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to z (1_{𝑜}) \in B$
52	1	xpsfval	$⊢ (z (\emptyset) \in A \land z (1_{𝑜}) \in B) \to z (\emptyset) F z (1_{𝑜}) = \{⟨\emptyset, z (\emptyset)⟩, ⟨1_{𝑜}, z (1_{𝑜})⟩\}$
53	50 51 52	syl2anc	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to z (\emptyset) F z (1_{𝑜}) = \{⟨\emptyset, z (\emptyset)⟩, ⟨1_{𝑜}, z (1_{𝑜})⟩\}$
54		ixpfn	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to z Fn 2_{𝑜}$
55		xpsfeq	$⊢ z Fn 2_{𝑜} \to \{⟨\emptyset, z (\emptyset)⟩, ⟨1_{𝑜}, z (1_{𝑜})⟩\} = z$
56	54 55	syl	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to \{⟨\emptyset, z (\emptyset)⟩, ⟨1_{𝑜}, z (1_{𝑜})⟩\} = z$
57	53 56	eqtr2d	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to z = z (\emptyset) F z (1_{𝑜})$
58		rspceov	$⊢ (z (\emptyset) \in A \land z (1_{𝑜}) \in B \land z = z (\emptyset) F z (1_{𝑜})) \to \exists a \in A \exists b \in B z = a F b$
59	50 51 57 58	syl3anc	$⊢ z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to \exists a \in A \exists b \in B z = a F b$
60	59	rgen	$⊢ \forall z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \exists a \in A \exists b \in B z = a F b$
61		foov	$⊢ F : A \times B \underset{onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (F : A \times B ⟶ \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \land \forall z \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \exists a \in A \exists b \in B z = a F b)$
62	6 60 61	mpbir2an	$⊢ F : A \times B \underset{onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
63		df-f1o	$⊢ F : A \times B \underset{1-1 onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (F : A \times B \underset{1-1}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \land F : A \times B \underset{onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B))$
64	48 62 63	mpbir2an	$⊢ F : A \times B \underset{1-1 onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$

Metamath Proof Explorer

Theorem xpsff1o

Proof