This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem enpr2d

Description: A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023) Avoid ax-un . (Revised by BTernaryTau, 23-Dec-2024)

Ref Expression
Hypotheses enpr2d.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
enpr2d.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
enpr2d.3 ⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
Assertion enpr2d ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )

Proof

Step Hyp Ref Expression
1 enpr2d.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2 enpr2d.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3 enpr2d.3 ⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
4 0ex ⊢ ∅ ∈ V
5 4 a1i ⊢ ( 𝜑 → ∅ ∈ V )
6 1oex ⊢ 1o ∈ V
7 6 a1i ⊢ ( 𝜑 → 1o ∈ V )
8 3 neqned ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
9 1n0 ⊢ 1o ≠ ∅
10 9 necomi ⊢ ∅ ≠ 1o
11 10 a1i ⊢ ( 𝜑 → ∅ ≠ 1o )
12 1 2 5 7 8 11 en2prd ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ { ∅ , 1o } )
13 df2o3 ⊢ 2o = { ∅ , 1o }
14 12 13 breqtrrdi ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )