Metamath Proof Explorer


Theorem xp1en

Description: One times a cardinal number. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion xp1en ( 𝐴𝑉 → ( 𝐴 × 1o ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 df1o2 1o = { ∅ }
2 1 xpeq2i ( 𝐴 × 1o ) = ( 𝐴 × { ∅ } )
3 0ex ∅ ∈ V
4 xpsneng ( ( 𝐴𝑉 ∧ ∅ ∈ V ) → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
5 3 4 mpan2 ( 𝐴𝑉 → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
6 2 5 eqbrtrid ( 𝐴𝑉 → ( 𝐴 × 1o ) ≈ 𝐴 )