bj-snsetex

Description: The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep . (Contributed by BJ, 6-Oct-2018)

		Ref	Expression
	Assertion	bj-snsetex	$⊢ A \in V \to \{x \| \{x\} \in A\} \in V$

Proof

Step	Hyp	Ref	Expression
1		elisset	$⊢ A \in V \to \exists y y = A$
2		eleq2	$⊢ y = A \to (\{x\} \in y \leftrightarrow \{x\} \in A)$
3	2	abbidv	$⊢ y = A \to \{x \| \{x\} \in y\} = \{x \| \{x\} \in A\}$
4		eleq1	$⊢ \{x \| \{x\} \in y\} = \{x \| \{x\} \in A\} \to (\{x \| \{x\} \in y\} \in V \leftrightarrow \{x \| \{x\} \in A\} \in V)$
5	4	biimpd	$⊢ \{x \| \{x\} \in y\} = \{x \| \{x\} \in A\} \to (\{x \| \{x\} \in y\} \in V \to \{x \| \{x\} \in A\} \in V)$
6	3 5	syl	$⊢ y = A \to (\{x \| \{x\} \in y\} \in V \to \{x \| \{x\} \in A\} \in V)$
7	6	eximi	$⊢ \exists y y = A \to \exists y (\{x \| \{x\} \in y\} \in V \to \{x \| \{x\} \in A\} \in V)$
8	1 7	syl	$⊢ A \in V \to \exists y (\{x \| \{x\} \in y\} \in V \to \{x \| \{x\} \in A\} \in V)$
9		bj-eximcom	$⊢ \exists y (\{x \| \{x\} \in y\} \in V \to \{x \| \{x\} \in A\} \in V) \to (\forall y \{x \| \{x\} \in y\} \in V \to \exists y \{x \| \{x\} \in A\} \in V)$
10	9	com12	$⊢ \forall y \{x \| \{x\} \in y\} \in V \to (\exists y (\{x \| \{x\} \in y\} \in V \to \{x \| \{x\} \in A\} \in V) \to \exists y \{x \| \{x\} \in A\} \in V)$
11		ax-rep	$⊢ \forall u \exists z \forall t (\forall z u = \{t\} \to t = z) \to \exists z \forall t (t \in z \leftrightarrow \exists u (u \in y \land \forall z u = \{t\}))$
12		19.3v	$⊢ \forall z u = \{t\} \leftrightarrow u = \{t\}$
13	12	sbbii	$⊢ [z/ t] \forall z u = \{t\} \leftrightarrow [z/ t] u = \{t\}$
14		sbsbc	$⊢ [z/ t] u = \{t\} \leftrightarrow \underset{˙}{[} z / t \underset{˙}{]} u = \{t\}$
15		sbceq2g	$⊢ z \in V \to (\underset{˙}{[} z / t \underset{˙}{]} u = \{t\} \leftrightarrow u = ⦋ z / t ⦌ \{t\})$
16	15	elv	$⊢ \underset{˙}{[} z / t \underset{˙}{]} u = \{t\} \leftrightarrow u = ⦋ z / t ⦌ \{t\}$
17	14 16	bitri	$⊢ [z/ t] u = \{t\} \leftrightarrow u = ⦋ z / t ⦌ \{t\}$
18		bj-csbsn	$⊢ ⦋ z / t ⦌ \{t\} = \{z\}$
19	18	eqeq2i	$⊢ u = ⦋ z / t ⦌ \{t\} \leftrightarrow u = \{z\}$
20	17 19	bitri	$⊢ [z/ t] u = \{t\} \leftrightarrow u = \{z\}$
21		eqtr2	$⊢ (u = \{t\} \land u = \{z\}) \to \{t\} = \{z\}$
22		vex	$⊢ t \in V$
23	22	sneqr	$⊢ \{t\} = \{z\} \to t = z$
24	21 23	syl	$⊢ (u = \{t\} \land u = \{z\}) \to t = z$
25	20 24	sylan2b	$⊢ (u = \{t\} \land [z/ t] u = \{t\}) \to t = z$
26	12 13 25	syl2anb	$⊢ (\forall z u = \{t\} \land [z/ t] \forall z u = \{t\}) \to t = z$
27	26	gen2	$⊢ \forall t \forall z ((\forall z u = \{t\} \land [z/ t] \forall z u = \{t\}) \to t = z)$
28		nfa1	$⊢ Ⅎ z \forall z u = \{t\}$
29	28	mo	$⊢ \exists z \forall t (\forall z u = \{t\} \to t = z) \leftrightarrow \forall t \forall z ((\forall z u = \{t\} \land [z/ t] \forall z u = \{t\}) \to t = z)$
30	27 29	mpbir	$⊢ \exists z \forall t (\forall z u = \{t\} \to t = z)$
31	11 30	mpg	$⊢ \exists z \forall t (t \in z \leftrightarrow \exists u (u \in y \land \forall z u = \{t\}))$
32		bj-sbel1	$⊢ [t/ x] \{x\} \in y \leftrightarrow ⦋ t / x ⦌ \{x\} \in y$
33		bj-csbsn	$⊢ ⦋ t / x ⦌ \{x\} = \{t\}$
34	33	eleq1i	$⊢ ⦋ t / x ⦌ \{x\} \in y \leftrightarrow \{t\} \in y$
35	32 34	bitri	$⊢ [t/ x] \{x\} \in y \leftrightarrow \{t\} \in y$
36		df-clab	$⊢ t \in \{x \| \{x\} \in y\} \leftrightarrow [t/ x] \{x\} \in y$
37	12	anbi2i	$⊢ (u \in y \land \forall z u = \{t\}) \leftrightarrow (u \in y \land u = \{t\})$
38		eleq1a	$⊢ u \in y \to (\{t\} = u \to \{t\} \in y)$
39	38	com12	$⊢ \{t\} = u \to (u \in y \to \{t\} \in y)$
40	39	eqcoms	$⊢ u = \{t\} \to (u \in y \to \{t\} \in y)$
41	40	imdistanri	$⊢ (u \in y \land u = \{t\}) \to (\{t\} \in y \land u = \{t\})$
42		eleq1a	$⊢ \{t\} \in y \to (u = \{t\} \to u \in y)$
43	42	impac	$⊢ (\{t\} \in y \land u = \{t\}) \to (u \in y \land u = \{t\})$
44	41 43	impbii	$⊢ (u \in y \land u = \{t\}) \leftrightarrow (\{t\} \in y \land u = \{t\})$
45	37 44	bitri	$⊢ (u \in y \land \forall z u = \{t\}) \leftrightarrow (\{t\} \in y \land u = \{t\})$
46	45	exbii	$⊢ \exists u (u \in y \land \forall z u = \{t\}) \leftrightarrow \exists u (\{t\} \in y \land u = \{t\})$
47		snex	$⊢ \{t\} \in V$
48	47	isseti	$⊢ \exists u u = \{t\}$
49		19.42v	$⊢ \exists u (\{t\} \in y \land u = \{t\}) \leftrightarrow (\{t\} \in y \land \exists u u = \{t\})$
50	48 49	mpbiran2	$⊢ \exists u (\{t\} \in y \land u = \{t\}) \leftrightarrow \{t\} \in y$
51	46 50	bitri	$⊢ \exists u (u \in y \land \forall z u = \{t\}) \leftrightarrow \{t\} \in y$
52	35 36 51	3bitr4ri	$⊢ \exists u (u \in y \land \forall z u = \{t\}) \leftrightarrow t \in \{x \| \{x\} \in y\}$
53	52	bibi2i	$⊢ (t \in z \leftrightarrow \exists u (u \in y \land \forall z u = \{t\})) \leftrightarrow (t \in z \leftrightarrow t \in \{x \| \{x\} \in y\})$
54	53	albii	$⊢ \forall t (t \in z \leftrightarrow \exists u (u \in y \land \forall z u = \{t\})) \leftrightarrow \forall t (t \in z \leftrightarrow t \in \{x \| \{x\} \in y\})$
55	54	exbii	$⊢ \exists z \forall t (t \in z \leftrightarrow \exists u (u \in y \land \forall z u = \{t\})) \leftrightarrow \exists z \forall t (t \in z \leftrightarrow t \in \{x \| \{x\} \in y\})$
56	31 55	mpbi	$⊢ \exists z \forall t (t \in z \leftrightarrow t \in \{x \| \{x\} \in y\})$
57		dfcleq	$⊢ z = \{x \| \{x\} \in y\} \leftrightarrow \forall t (t \in z \leftrightarrow t \in \{x \| \{x\} \in y\})$
58	57	exbii	$⊢ \exists z z = \{x \| \{x\} \in y\} \leftrightarrow \exists z \forall t (t \in z \leftrightarrow t \in \{x \| \{x\} \in y\})$
59	56 58	mpbir	$⊢ \exists z z = \{x \| \{x\} \in y\}$
60	59	issetri	$⊢ \{x \| \{x\} \in y\} \in V$
61	10 60	mpg	$⊢ \exists y (\{x \| \{x\} \in y\} \in V \to \{x \| \{x\} \in A\} \in V) \to \exists y \{x \| \{x\} \in A\} \in V$
62	8 61	syl	$⊢ A \in V \to \exists y \{x \| \{x\} \in A\} \in V$
63		ax5e	$⊢ \exists y \{x \| \{x\} \in A\} \in V \to \{x \| \{x\} \in A\} \in V$
64	62 63	syl	$⊢ A \in V \to \{x \| \{x\} \in A\} \in V$

Metamath Proof Explorer

Theorem bj-snsetex

Proof