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	$⊢ A \in V$
	xpsnen.2	$⊢ B \in V$
Assertion	xpsnen	$⊢ (A \times \{B\}) \approx A$

Proof

Step	Hyp	Ref	Expression
1		xpsnen.1	$⊢ A \in V$
2		xpsnen.2	$⊢ B \in V$
3		snex	$⊢ \{B\} \in V$
4	1 3	xpex	$⊢ A \times \{B\} \in V$
5		elxp	$⊢ y \in (A \times \{B\}) \leftrightarrow \exists x \exists z (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\}))$
6		inteq	$⊢ y = ⟨x, z⟩ \to ⋂ y = ⋂ ⟨x, z⟩$
7	6	inteqd	$⊢ y = ⟨x, z⟩ \to ⋂ ⋂ y = ⋂ ⋂ ⟨x, z⟩$
8		vex	$⊢ x \in V$
9		vex	$⊢ z \in V$
10	8 9	op1stb	$⊢ ⋂ ⋂ ⟨x, z⟩ = x$
11	7 10	eqtrdi	$⊢ y = ⟨x, z⟩ \to ⋂ ⋂ y = x$
12	11 8	eqeltrdi	$⊢ y = ⟨x, z⟩ \to ⋂ ⋂ y \in V$
13	12	adantr	$⊢ (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\})) \to ⋂ ⋂ y \in V$
14	13	exlimivv	$⊢ \exists x \exists z (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\})) \to ⋂ ⋂ y \in V$
15	5 14	sylbi	$⊢ y \in (A \times \{B\}) \to ⋂ ⋂ y \in V$
16		opex	$⊢ ⟨x, B⟩ \in V$
17	16	a1i	$⊢ x \in A \to ⟨x, B⟩ \in V$
18		eqvisset	$⊢ x = ⋂ ⋂ y \to ⋂ ⋂ y \in V$
19		ancom	$⊢ ((y = ⟨x, z⟩ \land x \in A) \land z \in \{B\}) \leftrightarrow (z \in \{B\} \land (y = ⟨x, z⟩ \land x \in A))$
20		anass	$⊢ ((y = ⟨x, z⟩ \land x \in A) \land z \in \{B\}) \leftrightarrow (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\}))$
21		velsn	$⊢ z \in \{B\} \leftrightarrow z = B$
22	21	anbi1i	$⊢ (z \in \{B\} \land (y = ⟨x, z⟩ \land x \in A)) \leftrightarrow (z = B \land (y = ⟨x, z⟩ \land x \in A))$
23	19 20 22	3bitr3i	$⊢ (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\})) \leftrightarrow (z = B \land (y = ⟨x, z⟩ \land x \in A))$
24	23	exbii	$⊢ \exists z (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\})) \leftrightarrow \exists z (z = B \land (y = ⟨x, z⟩ \land x \in A))$
25		opeq2	$⊢ z = B \to ⟨x, z⟩ = ⟨x, B⟩$
26	25	eqeq2d	$⊢ z = B \to (y = ⟨x, z⟩ \leftrightarrow y = ⟨x, B⟩)$
27	26	anbi1d	$⊢ z = B \to ((y = ⟨x, z⟩ \land x \in A) \leftrightarrow (y = ⟨x, B⟩ \land x \in A))$
28	2 27	ceqsexv	$⊢ \exists z (z = B \land (y = ⟨x, z⟩ \land x \in A)) \leftrightarrow (y = ⟨x, B⟩ \land x \in A)$
29		inteq	$⊢ y = ⟨x, B⟩ \to ⋂ y = ⋂ ⟨x, B⟩$
30	29	inteqd	$⊢ y = ⟨x, B⟩ \to ⋂ ⋂ y = ⋂ ⋂ ⟨x, B⟩$
31	8 2	op1stb	$⊢ ⋂ ⋂ ⟨x, B⟩ = x$
32	30 31	eqtr2di	$⊢ y = ⟨x, B⟩ \to x = ⋂ ⋂ y$
33	32	pm4.71ri	$⊢ y = ⟨x, B⟩ \leftrightarrow (x = ⋂ ⋂ y \land y = ⟨x, B⟩)$
34	33	anbi1i	$⊢ (y = ⟨x, B⟩ \land x \in A) \leftrightarrow ((x = ⋂ ⋂ y \land y = ⟨x, B⟩) \land x \in A)$
35		anass	$⊢ ((x = ⋂ ⋂ y \land y = ⟨x, B⟩) \land x \in A) \leftrightarrow (x = ⋂ ⋂ y \land (y = ⟨x, B⟩ \land x \in A))$
36	34 35	bitri	$⊢ (y = ⟨x, B⟩ \land x \in A) \leftrightarrow (x = ⋂ ⋂ y \land (y = ⟨x, B⟩ \land x \in A))$
37	24 28 36	3bitri	$⊢ \exists z (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\})) \leftrightarrow (x = ⋂ ⋂ y \land (y = ⟨x, B⟩ \land x \in A))$
38	37	exbii	$⊢ \exists x \exists z (y = ⟨x, z⟩ \land (x \in A \land z \in \{B\})) \leftrightarrow \exists x (x = ⋂ ⋂ y \land (y = ⟨x, B⟩ \land x \in A))$
39	5 38	bitri	$⊢ y \in (A \times \{B\}) \leftrightarrow \exists x (x = ⋂ ⋂ y \land (y = ⟨x, B⟩ \land x \in A))$
40		opeq1	$⊢ x = ⋂ ⋂ y \to ⟨x, B⟩ = ⟨⋂ ⋂ y, B⟩$
41	40	eqeq2d	$⊢ x = ⋂ ⋂ y \to (y = ⟨x, B⟩ \leftrightarrow y = ⟨⋂ ⋂ y, B⟩)$
42		eleq1	$⊢ x = ⋂ ⋂ y \to (x \in A \leftrightarrow ⋂ ⋂ y \in A)$
43	41 42	anbi12d	$⊢ x = ⋂ ⋂ y \to ((y = ⟨x, B⟩ \land x \in A) \leftrightarrow (y = ⟨⋂ ⋂ y, B⟩ \land ⋂ ⋂ y \in A))$
44	43	ceqsexgv	$⊢ ⋂ ⋂ y \in V \to (\exists x (x = ⋂ ⋂ y \land (y = ⟨x, B⟩ \land x \in A)) \leftrightarrow (y = ⟨⋂ ⋂ y, B⟩ \land ⋂ ⋂ y \in A))$
45	39 44	syl5bb	$⊢ ⋂ ⋂ y \in V \to (y \in (A \times \{B\}) \leftrightarrow (y = ⟨⋂ ⋂ y, B⟩ \land ⋂ ⋂ y \in A))$
46	18 45	syl	$⊢ x = ⋂ ⋂ y \to (y \in (A \times \{B\}) \leftrightarrow (y = ⟨⋂ ⋂ y, B⟩ \land ⋂ ⋂ y \in A))$
47	46	pm5.32ri	$⊢ (y \in (A \times \{B\}) \land x = ⋂ ⋂ y) \leftrightarrow ((y = ⟨⋂ ⋂ y, B⟩ \land ⋂ ⋂ y \in A) \land x = ⋂ ⋂ y)$
48	32	adantr	$⊢ (y = ⟨x, B⟩ \land x \in A) \to x = ⋂ ⋂ y$
49	48	pm4.71i	$⊢ (y = ⟨x, B⟩ \land x \in A) \leftrightarrow ((y = ⟨x, B⟩ \land x \in A) \land x = ⋂ ⋂ y)$
50	43	pm5.32ri	$⊢ ((y = ⟨x, B⟩ \land x \in A) \land x = ⋂ ⋂ y) \leftrightarrow ((y = ⟨⋂ ⋂ y, B⟩ \land ⋂ ⋂ y \in A) \land x = ⋂ ⋂ y)$
51	49 50	bitr2i	$⊢ ((y = ⟨⋂ ⋂ y, B⟩ \land ⋂ ⋂ y \in A) \land x = ⋂ ⋂ y) \leftrightarrow (y = ⟨x, B⟩ \land x \in A)$
52		ancom	$⊢ (y = ⟨x, B⟩ \land x \in A) \leftrightarrow (x \in A \land y = ⟨x, B⟩)$
53	47 51 52	3bitri	$⊢ (y \in (A \times \{B\}) \land x = ⋂ ⋂ y) \leftrightarrow (x \in A \land y = ⟨x, B⟩)$
54	4 1 15 17 53	en2i	$⊢ (A \times \{B\}) \approx A$

Metamath Proof Explorer

Theorem xpsnen

Proof