Description: A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of Mendelson p. 254. (Contributed by NM, 22-Oct-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | xpsneng | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × { 𝐵 } ) ≈ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1 | ⊢ ( 𝑥 = 𝐴 → ( 𝑥 × { 𝑦 } ) = ( 𝐴 × { 𝑦 } ) ) | |
2 | id | ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 ) | |
3 | 1 2 | breq12d | ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 × { 𝑦 } ) ≈ 𝑥 ↔ ( 𝐴 × { 𝑦 } ) ≈ 𝐴 ) ) |
4 | sneq | ⊢ ( 𝑦 = 𝐵 → { 𝑦 } = { 𝐵 } ) | |
5 | 4 | xpeq2d | ⊢ ( 𝑦 = 𝐵 → ( 𝐴 × { 𝑦 } ) = ( 𝐴 × { 𝐵 } ) ) |
6 | 5 | breq1d | ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 × { 𝑦 } ) ≈ 𝐴 ↔ ( 𝐴 × { 𝐵 } ) ≈ 𝐴 ) ) |
7 | vex | ⊢ 𝑥 ∈ V | |
8 | vex | ⊢ 𝑦 ∈ V | |
9 | 7 8 | xpsnen | ⊢ ( 𝑥 × { 𝑦 } ) ≈ 𝑥 |
10 | 3 6 9 | vtocl2g | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × { 𝐵 } ) ≈ 𝐴 ) |