Metamath Proof Explorer

Theorem prproropen

Description: 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, are equinumerous. (Contributed by AV, 15-Mar-2023)

Ref Expression
Hypotheses prproropf1o.o ⊢ O = R ∩ V × V
prproropf1o.p ⊢ P = p ∈ 𝒫 V | p = 2
Assertion prproropen ⊢ V ∈ W ∧ R Or V → O ≈ P

Proof

Step Hyp Ref Expression
1 prproropf1o.o ⊢ O = R ∩ V × V
2 prproropf1o.p ⊢ P = p ∈ 𝒫 V | p = 2
3 pwexg ⊢ V ∈ W → 𝒫 V ∈ V
4 2 3 rabexd ⊢ V ∈ W → P ∈ V
5 4 adantr ⊢ V ∈ W ∧ R Or V → P ∈ V
6 5 mptexd ⊢ V ∈ W ∧ R Or V → p ∈ P ⟼ sup p V R sup p V R ∈ V
7 eqid ⊢ p ∈ P ⟼ sup p V R sup p V R = p ∈ P ⟼ sup p V R sup p V R
8 1 2 7 prproropf1o ⊢ R Or V → p ∈ P ⟼ sup p V R sup p V R : P ⟶ 1-1 onto O
9 8 adantl ⊢ V ∈ W ∧ R Or V → p ∈ P ⟼ sup p V R sup p V R : P ⟶ 1-1 onto O
10 f1oeq1 ⊢ f = p ∈ P ⟼ sup p V R sup p V R → f : P ⟶ 1-1 onto O ↔ p ∈ P ⟼ sup p V R sup p V R : P ⟶ 1-1 onto O
11 6 9 10 spcedv ⊢ V ∈ W ∧ R Or V → ∃ f f : P ⟶ 1-1 onto O
12 ensymb ⊢ O ≈ P ↔ P ≈ O
13 bren ⊢ P ≈ O ↔ ∃ f f : P ⟶ 1-1 onto O
14 12 13 bitri ⊢ O ≈ P ↔ ∃ f f : P ⟶ 1-1 onto O
15 11 14 sylibr ⊢ V ∈ W ∧ R Or V → O ≈ P