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 syl6eq ⊢ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ → ∩ ∩ 𝑦 = 𝑥 )
12 11 8 syl6eqel ⊢ ( 𝑦 = ⟨ 𝑥 , 𝑧 ⟩ → ∩ ∩ 𝑦 ∈ 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 syl6req ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ → 𝑥 = ∩ ∩ 𝑦 )
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 ⊢ ( 𝐴 × { 𝐵 } ) ≈ 𝐴