Metamath Proof Explorer


Theorem xpsnen

Description: A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of Mendelson p. 254. (Contributed by NM, 4-Jan-2004) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Hypotheses xpsnen.1 𝐴 ∈ V
xpsnen.2 𝐵 ∈ V
Assertion xpsnen ( 𝐴 × { 𝐵 } ) ≈ 𝐴

Proof

Step Hyp Ref Expression
1 xpsnen.1 𝐴 ∈ V
2 xpsnen.2 𝐵 ∈ V
3 snex { 𝐵 } ∈ V
4 1 3 xpex ( 𝐴 × { 𝐵 } ) ∈ V
5 elxp ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ∃ 𝑥𝑧 ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) )
6 inteq ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ → 𝑦 = 𝑥 , 𝑧 ⟩ )
7 6 inteqd ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ → 𝑦 = 𝑥 , 𝑧 ⟩ )
8 vex 𝑥 ∈ V
9 vex 𝑧 ∈ V
10 8 9 op1stb 𝑥 , 𝑧 ⟩ = 𝑥
11 7 10 eqtrdi ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ → 𝑦 = 𝑥 )
12 11 8 eqeltrdi ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ → 𝑦 ∈ V )
13 12 adantr ( ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) → 𝑦 ∈ V )
14 13 exlimivv ( ∃ 𝑥𝑧 ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) → 𝑦 ∈ V )
15 5 14 sylbi ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) → 𝑦 ∈ V )
16 opex 𝑥 , 𝐵 ⟩ ∈ V
17 16 a1i ( 𝑥𝐴 → ⟨ 𝑥 , 𝐵 ⟩ ∈ V )
18 eqvisset ( 𝑥 = 𝑦 𝑦 ∈ V )
19 ancom ( ( ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ∧ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑧 ∈ { 𝐵 } ∧ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ) )
20 anass ( ( ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ∧ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) )
21 velsn ( 𝑧 ∈ { 𝐵 } ↔ 𝑧 = 𝐵 )
22 21 anbi1i ( ( 𝑧 ∈ { 𝐵 } ∧ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ) ↔ ( 𝑧 = 𝐵 ∧ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ) )
23 19 20 22 3bitr3i ( ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) ↔ ( 𝑧 = 𝐵 ∧ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ) )
24 23 exbii ( ∃ 𝑧 ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝐵 ∧ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ) )
25 opeq2 ( 𝑧 = 𝐵 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝐵 ⟩ )
26 25 eqeq2d ( 𝑧 = 𝐵 → ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ↔ 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ) )
27 26 anbi1d ( 𝑧 = 𝐵 → ( ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ↔ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ) )
28 2 27 ceqsexv ( ∃ 𝑧 ( 𝑧 = 𝐵 ∧ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥𝐴 ) ) ↔ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) )
29 inteq ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ → 𝑦 = 𝑥 , 𝐵 ⟩ )
30 29 inteqd ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ → 𝑦 = 𝑥 , 𝐵 ⟩ )
31 8 2 op1stb 𝑥 , 𝐵 ⟩ = 𝑥
32 30 31 eqtr2di ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ → 𝑥 = 𝑦 )
33 32 pm4.71ri ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ↔ ( 𝑥 = 𝑦𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ) )
34 33 anbi1i ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ↔ ( ( 𝑥 = 𝑦𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ) ∧ 𝑥𝐴 ) )
35 anass ( ( ( 𝑥 = 𝑦𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ) ∧ 𝑥𝐴 ) ↔ ( 𝑥 = 𝑦 ∧ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ) )
36 34 35 bitri ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ↔ ( 𝑥 = 𝑦 ∧ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ) )
37 24 28 36 3bitri ( ∃ 𝑧 ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) ↔ ( 𝑥 = 𝑦 ∧ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ) )
38 37 exbii ( ∃ 𝑥𝑧 ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ ∧ ( 𝑥𝐴𝑧 ∈ { 𝐵 } ) ) ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ) )
39 5 38 bitri ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ) )
40 opeq1 ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝐵 ⟩ = ⟨ 𝑦 , 𝐵 ⟩ )
41 40 eqeq2d ( 𝑥 = 𝑦 → ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ↔ 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ) )
42 eleq1 ( 𝑥 = 𝑦 → ( 𝑥𝐴 𝑦𝐴 ) )
43 41 42 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ↔ ( 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ∧ 𝑦𝐴 ) ) )
44 43 ceqsexgv ( 𝑦 ∈ V → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ) ↔ ( 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ∧ 𝑦𝐴 ) ) )
45 39 44 syl5bb ( 𝑦 ∈ V → ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ( 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ∧ 𝑦𝐴 ) ) )
46 18 45 syl ( 𝑥 = 𝑦 → ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ( 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ∧ 𝑦𝐴 ) ) )
47 46 pm5.32ri ( ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ∧ 𝑥 = 𝑦 ) ↔ ( ( 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ∧ 𝑦𝐴 ) ∧ 𝑥 = 𝑦 ) )
48 32 adantr ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) → 𝑥 = 𝑦 )
49 48 pm4.71i ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ↔ ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ∧ 𝑥 = 𝑦 ) )
50 43 pm5.32ri ( ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ∧ 𝑥 = 𝑦 ) ↔ ( ( 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ∧ 𝑦𝐴 ) ∧ 𝑥 = 𝑦 ) )
51 49 50 bitr2i ( ( ( 𝑦 = ⟨ 𝑦 , 𝐵 ⟩ ∧ 𝑦𝐴 ) ∧ 𝑥 = 𝑦 ) ↔ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) )
52 ancom ( ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ∧ 𝑥𝐴 ) ↔ ( 𝑥𝐴𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ) )
53 47 51 52 3bitri ( ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ∧ 𝑥 = 𝑦 ) ↔ ( 𝑥𝐴𝑦 = ⟨ 𝑥 , 𝐵 ⟩ ) )
54 4 1 15 17 53 en2i ( 𝐴 × { 𝐵 } ) ≈ 𝐴