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	bitrid	⊢ ( ∩ ∩ 𝑦 ∈ 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	⊢ ( 𝐴 × { 𝐵 } ) ≈ 𝐴

Metamath Proof Explorer

Theorem xpsnen

Proof