prproropf1o

Description: There is a bijection between the set of proper pairs and the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component. (Contributed by AV, 15-Mar-2023)

	Ref	Expression
Hypotheses	prproropf1o.o	$⊢ O = R \cap (V \times V)$
	prproropf1o.p	$⊢ P = \{p \in 𝒫 V \| \|p\| = 2\}$
	prproropf1o.f	$⊢ F = (p \in P ⟼ ⟨inf (p, V, R), sup (p, V, R)⟩)$
Assertion	prproropf1o	$⊢ R Or V \to F : P \underset{1-1 onto}{⟶} O$

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	$⊢ O = R \cap (V \times V)$
2		prproropf1o.p	$⊢ P = \{p \in 𝒫 V \| \|p\| = 2\}$
3		prproropf1o.f	$⊢ F = (p \in P ⟼ ⟨inf (p, V, R), sup (p, V, R)⟩)$
4	1 2	prproropf1olem2	$⊢ (R Or V \land w \in P) \to ⟨inf (w, V, R), sup (w, V, R)⟩ \in O$
5		infeq1	$⊢ p = w \to inf (p, V, R) = inf (w, V, R)$
6		supeq1	$⊢ p = w \to sup (p, V, R) = sup (w, V, R)$
7	5 6	opeq12d	$⊢ p = w \to ⟨inf (p, V, R), sup (p, V, R)⟩ = ⟨inf (w, V, R), sup (w, V, R)⟩$
8	7	cbvmptv	$⊢ (p \in P ⟼ ⟨inf (p, V, R), sup (p, V, R)⟩) = (w \in P ⟼ ⟨inf (w, V, R), sup (w, V, R)⟩)$
9	3 8	eqtri	$⊢ F = (w \in P ⟼ ⟨inf (w, V, R), sup (w, V, R)⟩)$
10	4 9	fmptd	$⊢ R Or V \to F : P ⟶ O$
11		3ancomb	$⊢ (R Or V \land w \in P \land z \in P) \leftrightarrow (R Or V \land z \in P \land w \in P)$
12		3anass	$⊢ (R Or V \land z \in P \land w \in P) \leftrightarrow (R Or V \land (z \in P \land w \in P))$
13	11 12	bitri	$⊢ (R Or V \land w \in P \land z \in P) \leftrightarrow (R Or V \land (z \in P \land w \in P))$
14	1 2 3	prproropf1olem4	$⊢ (R Or V \land w \in P \land z \in P) \to (F (z) = F (w) \to z = w)$
15	13 14	sylbir	$⊢ (R Or V \land (z \in P \land w \in P)) \to (F (z) = F (w) \to z = w)$
16	15	ralrimivva	$⊢ R Or V \to \forall z \in P \forall w \in P (F (z) = F (w) \to z = w)$
17		dff13	$⊢ F : P \underset{1-1}{⟶} O \leftrightarrow (F : P ⟶ O \land \forall z \in P \forall w \in P (F (z) = F (w) \to z = w))$
18	10 16 17	sylanbrc	$⊢ R Or V \to F : P \underset{1-1}{⟶} O$
19	1 2	prproropf1olem1	$⊢ (R Or V \land w \in O) \to \{1^{st} (w), 2^{nd} (w)\} \in P$
20		fveq2	$⊢ z = \{1^{st} (w), 2^{nd} (w)\} \to F (z) = F (\{1^{st} (w), 2^{nd} (w)\})$
21	20	eqeq2d	$⊢ z = \{1^{st} (w), 2^{nd} (w)\} \to (w = F (z) \leftrightarrow w = F (\{1^{st} (w), 2^{nd} (w)\}))$
22	21	adantl	$⊢ ((R Or V \land w \in O) \land z = \{1^{st} (w), 2^{nd} (w)\}) \to (w = F (z) \leftrightarrow w = F (\{1^{st} (w), 2^{nd} (w)\}))$
23	1 2 3	prproropf1olem3	$⊢ (R Or V \land w \in O) \to F (\{1^{st} (w), 2^{nd} (w)\}) = ⟨1^{st} (w), 2^{nd} (w)⟩$
24	1	prproropf1olem0	$⊢ w \in O \leftrightarrow (w = ⟨1^{st} (w), 2^{nd} (w)⟩ \land (1^{st} (w) \in V \land 2^{nd} (w) \in V) \land 1^{st} (w) R 2^{nd} (w))$
25	24	simp1bi	$⊢ w \in O \to w = ⟨1^{st} (w), 2^{nd} (w)⟩$
26	25	eqcomd	$⊢ w \in O \to ⟨1^{st} (w), 2^{nd} (w)⟩ = w$
27	26	adantl	$⊢ (R Or V \land w \in O) \to ⟨1^{st} (w), 2^{nd} (w)⟩ = w$
28	23 27	eqtr2d	$⊢ (R Or V \land w \in O) \to w = F (\{1^{st} (w), 2^{nd} (w)\})$
29	19 22 28	rspcedvd	$⊢ (R Or V \land w \in O) \to \exists z \in P w = F (z)$
30	29	ralrimiva	$⊢ R Or V \to \forall w \in O \exists z \in P w = F (z)$
31		dffo3	$⊢ F : P \underset{onto}{⟶} O \leftrightarrow (F : P ⟶ O \land \forall w \in O \exists z \in P w = F (z))$
32	10 30 31	sylanbrc	$⊢ R Or V \to F : P \underset{onto}{⟶} O$
33		df-f1o	$⊢ F : P \underset{1-1 onto}{⟶} O \leftrightarrow (F : P \underset{1-1}{⟶} O \land F : P \underset{onto}{⟶} O)$
34	18 32 33	sylanbrc	$⊢ R Or V \to F : P \underset{1-1 onto}{⟶} O$

Metamath Proof Explorer

Theorem prproropf1o

Proof