projf1o

Description: A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	projf1o.1	$⊢ φ \to A \in V$
	projf1o.2	$⊢ F = (x \in B ⟼ ⟨A, x⟩)$
Assertion	projf1o	$⊢ φ \to F : B \underset{1-1 onto}{⟶} \{A\} \times B$

Proof

Step	Hyp	Ref	Expression
1		projf1o.1	$⊢ φ \to A \in V$
2		projf1o.2	$⊢ F = (x \in B ⟼ ⟨A, x⟩)$
3		snidg	$⊢ A \in V \to A \in \{A\}$
4	1 3	syl	$⊢ φ \to A \in \{A\}$
5	4	adantr	$⊢ (φ \land y \in B) \to A \in \{A\}$
6		simpr	$⊢ (φ \land y \in B) \to y \in B$
7	5 6	opelxpd	$⊢ (φ \land y \in B) \to ⟨A, y⟩ \in (\{A\} \times B)$
8		opeq2	$⊢ x = y \to ⟨A, x⟩ = ⟨A, y⟩$
9	8	cbvmptv	$⊢ (x \in B ⟼ ⟨A, x⟩) = (y \in B ⟼ ⟨A, y⟩)$
10	2 9	eqtri	$⊢ F = (y \in B ⟼ ⟨A, y⟩)$
11	7 10	fmptd	$⊢ φ \to F : B ⟶ \{A\} \times B$
12		simpl1	$⊢ ((φ \land y \in B \land z \in B) \land F (y) = F (z)) \to φ$
13	2 8 6 7	fvmptd3	$⊢ (φ \land y \in B) \to F (y) = ⟨A, y⟩$
14	13	eqcomd	$⊢ (φ \land y \in B) \to ⟨A, y⟩ = F (y)$
15	14	3adant3	$⊢ (φ \land y \in B \land z \in B) \to ⟨A, y⟩ = F (y)$
16	15	adantr	$⊢ ((φ \land y \in B \land z \in B) \land F (y) = F (z)) \to ⟨A, y⟩ = F (y)$
17		simpr	$⊢ ((φ \land y \in B \land z \in B) \land F (y) = F (z)) \to F (y) = F (z)$
18		opeq2	$⊢ y = z \to ⟨A, y⟩ = ⟨A, z⟩$
19		simpr	$⊢ (φ \land z \in B) \to z \in B$
20		opex	$⊢ ⟨A, z⟩ \in V$
21	20	a1i	$⊢ (φ \land z \in B) \to ⟨A, z⟩ \in V$
22	10 18 19 21	fvmptd3	$⊢ (φ \land z \in B) \to F (z) = ⟨A, z⟩$
23	22	3adant2	$⊢ (φ \land y \in B \land z \in B) \to F (z) = ⟨A, z⟩$
24	23	adantr	$⊢ ((φ \land y \in B \land z \in B) \land F (y) = F (z)) \to F (z) = ⟨A, z⟩$
25	16 17 24	3eqtrd	$⊢ ((φ \land y \in B \land z \in B) \land F (y) = F (z)) \to ⟨A, y⟩ = ⟨A, z⟩$
26		vex	$⊢ z \in V$
27	26	a1i	$⊢ φ \to z \in V$
28		opthg2	$⊢ (A \in V \land z \in V) \to (⟨A, y⟩ = ⟨A, z⟩ \leftrightarrow (A = A \land y = z))$
29	1 27 28	syl2anc	$⊢ φ \to (⟨A, y⟩ = ⟨A, z⟩ \leftrightarrow (A = A \land y = z))$
30	29	simplbda	$⊢ (φ \land ⟨A, y⟩ = ⟨A, z⟩) \to y = z$
31	12 25 30	syl2anc	$⊢ ((φ \land y \in B \land z \in B) \land F (y) = F (z)) \to y = z$
32	31	ex	$⊢ (φ \land y \in B \land z \in B) \to (F (y) = F (z) \to y = z)$
33	32	3expb	$⊢ (φ \land (y \in B \land z \in B)) \to (F (y) = F (z) \to y = z)$
34	33	ralrimivva	$⊢ φ \to \forall y \in B \forall z \in B (F (y) = F (z) \to y = z)$
35		dff13	$⊢ F : B \underset{1-1}{⟶} \{A\} \times B \leftrightarrow (F : B ⟶ \{A\} \times B \land \forall y \in B \forall z \in B (F (y) = F (z) \to y = z))$
36	11 34 35	sylanbrc	$⊢ φ \to F : B \underset{1-1}{⟶} \{A\} \times B$
37		elsnxp	$⊢ A \in V \to (z \in (\{A\} \times B) \leftrightarrow \exists y \in B z = ⟨A, y⟩)$
38	1 37	syl	$⊢ φ \to (z \in (\{A\} \times B) \leftrightarrow \exists y \in B z = ⟨A, y⟩)$
39	38	biimpa	$⊢ (φ \land z \in (\{A\} \times B)) \to \exists y \in B z = ⟨A, y⟩$
40	13	adantr	$⊢ ((φ \land y \in B) \land z = ⟨A, y⟩) \to F (y) = ⟨A, y⟩$
41		id	$⊢ z = ⟨A, y⟩ \to z = ⟨A, y⟩$
42	41	eqcomd	$⊢ z = ⟨A, y⟩ \to ⟨A, y⟩ = z$
43	42	adantl	$⊢ ((φ \land y \in B) \land z = ⟨A, y⟩) \to ⟨A, y⟩ = z$
44	40 43	eqtr2d	$⊢ ((φ \land y \in B) \land z = ⟨A, y⟩) \to z = F (y)$
45	44	ex	$⊢ (φ \land y \in B) \to (z = ⟨A, y⟩ \to z = F (y))$
46	45	adantlr	$⊢ ((φ \land z \in (\{A\} \times B)) \land y \in B) \to (z = ⟨A, y⟩ \to z = F (y))$
47	46	reximdva	$⊢ (φ \land z \in (\{A\} \times B)) \to (\exists y \in B z = ⟨A, y⟩ \to \exists y \in B z = F (y))$
48	39 47	mpd	$⊢ (φ \land z \in (\{A\} \times B)) \to \exists y \in B z = F (y)$
49	48	ralrimiva	$⊢ φ \to \forall z \in (\{A\} \times B) \exists y \in B z = F (y)$
50		dffo3	$⊢ F : B \underset{onto}{⟶} \{A\} \times B \leftrightarrow (F : B ⟶ \{A\} \times B \land \forall z \in (\{A\} \times B) \exists y \in B z = F (y))$
51	11 49 50	sylanbrc	$⊢ φ \to F : B \underset{onto}{⟶} \{A\} \times B$
52		df-f1o	$⊢ F : B \underset{1-1 onto}{⟶} \{A\} \times B \leftrightarrow (F : B \underset{1-1}{⟶} \{A\} \times B \land F : B \underset{onto}{⟶} \{A\} \times B)$
53	36 51 52	sylanbrc	$⊢ φ \to F : B \underset{1-1 onto}{⟶} \{A\} \times B$

Metamath Proof Explorer

Theorem projf1o

Proof