Theorem 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	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elisset	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 𝑦 = 𝐴 )
2		eleq2	⊢ ( 𝑦 = 𝐴 → ( { 𝑥 } ∈ 𝑦 ↔ { 𝑥 } ∈ 𝐴 ) )
3	2	abbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } = { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } )
4		eleq1	⊢ ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } = { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } → ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V ↔ { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) )
5	4	biimpd	⊢ ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } = { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } → ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) )
6	3 5	syl	⊢ ( 𝑦 = 𝐴 → ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) )
7	6	eximi	⊢ ( ∃ 𝑦 𝑦 = 𝐴 → ∃ 𝑦 ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) )
8		bj-eximcom	⊢ ( ∃ 𝑦 ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) → ( ∀ 𝑦 { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → ∃ 𝑦 { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) )
9	8	com12	⊢ ( ∀ 𝑦 { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → ( ∃ 𝑦 ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) → ∃ 𝑦 { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) )
10		ax-rep	⊢ ( ∀ 𝑢 ∃ 𝑧 ∀ 𝑡 ( ∀ 𝑧 𝑢 = { 𝑡 } → 𝑡 = 𝑧 ) → ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ) )
11		19.3v	⊢ ( ∀ 𝑧 𝑢 = { 𝑡 } ↔ 𝑢 = { 𝑡 } )
12	11	sbbii	⊢ ( [ 𝑧 / 𝑡 ] ∀ 𝑧 𝑢 = { 𝑡 } ↔ [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } )
13		sbsbc	⊢ ( [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } ↔ [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } )
14		sbceq2g	⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } ↔ 𝑢 = ⦋ 𝑧 / 𝑡 ⦌ { 𝑡 } ) )
15	14	elv	⊢ ( [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } ↔ 𝑢 = ⦋ 𝑧 / 𝑡 ⦌ { 𝑡 } )
16	13 15	bitri	⊢ ( [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } ↔ 𝑢 = ⦋ 𝑧 / 𝑡 ⦌ { 𝑡 } )
17		bj-csbsn	⊢ ⦋ 𝑧 / 𝑡 ⦌ { 𝑡 } = { 𝑧 }
18	17	eqeq2i	⊢ ( 𝑢 = ⦋ 𝑧 / 𝑡 ⦌ { 𝑡 } ↔ 𝑢 = { 𝑧 } )
19	16 18	bitri	⊢ ( [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } ↔ 𝑢 = { 𝑧 } )
20		eqtr2	⊢ ( ( 𝑢 = { 𝑡 } ∧ 𝑢 = { 𝑧 } ) → { 𝑡 } = { 𝑧 } )
21		vex	⊢ 𝑡 ∈ V
22	21	sneqr	⊢ ( { 𝑡 } = { 𝑧 } → 𝑡 = 𝑧 )
23	20 22	syl	⊢ ( ( 𝑢 = { 𝑡 } ∧ 𝑢 = { 𝑧 } ) → 𝑡 = 𝑧 )
24	19 23	sylan2b	⊢ ( ( 𝑢 = { 𝑡 } ∧ [ 𝑧 / 𝑡 ] 𝑢 = { 𝑡 } ) → 𝑡 = 𝑧 )
25	11 12 24	syl2anb	⊢ ( ( ∀ 𝑧 𝑢 = { 𝑡 } ∧ [ 𝑧 / 𝑡 ] ∀ 𝑧 𝑢 = { 𝑡 } ) → 𝑡 = 𝑧 )
26	25	gen2	⊢ ∀ 𝑡 ∀ 𝑧 ( ( ∀ 𝑧 𝑢 = { 𝑡 } ∧ [ 𝑧 / 𝑡 ] ∀ 𝑧 𝑢 = { 𝑡 } ) → 𝑡 = 𝑧 )
27		nfa1	⊢ Ⅎ 𝑧 ∀ 𝑧 𝑢 = { 𝑡 }
28	27	mo	⊢ ( ∃ 𝑧 ∀ 𝑡 ( ∀ 𝑧 𝑢 = { 𝑡 } → 𝑡 = 𝑧 ) ↔ ∀ 𝑡 ∀ 𝑧 ( ( ∀ 𝑧 𝑢 = { 𝑡 } ∧ [ 𝑧 / 𝑡 ] ∀ 𝑧 𝑢 = { 𝑡 } ) → 𝑡 = 𝑧 ) )
29	26 28	mpbir	⊢ ∃ 𝑧 ∀ 𝑡 ( ∀ 𝑧 𝑢 = { 𝑡 } → 𝑡 = 𝑧 )
30	10 29	mpg	⊢ ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) )
31		bj-sbel1	⊢ ( [ 𝑡 / 𝑥 ] { 𝑥 } ∈ 𝑦 ↔ ⦋ 𝑡 / 𝑥 ⦌ { 𝑥 } ∈ 𝑦 )
32		bj-csbsn	⊢ ⦋ 𝑡 / 𝑥 ⦌ { 𝑥 } = { 𝑡 }
33	32	eleq1i	⊢ ( ⦋ 𝑡 / 𝑥 ⦌ { 𝑥 } ∈ 𝑦 ↔ { 𝑡 } ∈ 𝑦 )
34	31 33	bitri	⊢ ( [ 𝑡 / 𝑥 ] { 𝑥 } ∈ 𝑦 ↔ { 𝑡 } ∈ 𝑦 )
35		df-clab	⊢ ( 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ↔ [ 𝑡 / 𝑥 ] { 𝑥 } ∈ 𝑦 )
36	11	anbi2i	⊢ ( ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ↔ ( 𝑢 ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) )
37		eleq1a	⊢ ( 𝑢 ∈ 𝑦 → ( { 𝑡 } = 𝑢 → { 𝑡 } ∈ 𝑦 ) )
38	37	com12	⊢ ( { 𝑡 } = 𝑢 → ( 𝑢 ∈ 𝑦 → { 𝑡 } ∈ 𝑦 ) )
39	38	eqcoms	⊢ ( 𝑢 = { 𝑡 } → ( 𝑢 ∈ 𝑦 → { 𝑡 } ∈ 𝑦 ) )
40	39	imdistanri	⊢ ( ( 𝑢 ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) → ( { 𝑡 } ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) )
41		eleq1a	⊢ ( { 𝑡 } ∈ 𝑦 → ( 𝑢 = { 𝑡 } → 𝑢 ∈ 𝑦 ) )
42	41	impac	⊢ ( ( { 𝑡 } ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) → ( 𝑢 ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) )
43	40 42	impbii	⊢ ( ( 𝑢 ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) ↔ ( { 𝑡 } ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) )
44	36 43	bitri	⊢ ( ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ↔ ( { 𝑡 } ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) )
45	44	exbii	⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ↔ ∃ 𝑢 ( { 𝑡 } ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) )
46		vsnex	⊢ { 𝑡 } ∈ V
47	46	isseti	⊢ ∃ 𝑢 𝑢 = { 𝑡 }
48		19.42v	⊢ ( ∃ 𝑢 ( { 𝑡 } ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) ↔ ( { 𝑡 } ∈ 𝑦 ∧ ∃ 𝑢 𝑢 = { 𝑡 } ) )
49	47 48	mpbiran2	⊢ ( ∃ 𝑢 ( { 𝑡 } ∈ 𝑦 ∧ 𝑢 = { 𝑡 } ) ↔ { 𝑡 } ∈ 𝑦 )
50	45 49	bitri	⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ↔ { 𝑡 } ∈ 𝑦 )
51	34 35 50	3bitr4ri	⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ↔ 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } )
52	51	bibi2i	⊢ ( ( 𝑡 ∈ 𝑧 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ) ↔ ( 𝑡 ∈ 𝑧 ↔ 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ) )
53	52	albii	⊢ ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ) )
54	53	exbii	⊢ ( ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ∀ 𝑧 𝑢 = { 𝑡 } ) ) ↔ ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ) )
55	30 54	mpbi	⊢ ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } )
56		dfcleq	⊢ ( 𝑧 = { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ) )
57	56	exbii	⊢ ( ∃ 𝑧 𝑧 = { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ↔ ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ 𝑡 ∈ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ) )
58	55 57	mpbir	⊢ ∃ 𝑧 𝑧 = { 𝑥 ∣ { 𝑥 } ∈ 𝑦 }
59	58	issetri	⊢ { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V
60	9 59	mpg	⊢ ( ∃ 𝑦 ( { 𝑥 ∣ { 𝑥 } ∈ 𝑦 } ∈ V → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V ) → ∃ 𝑦 { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V )
61		ax5e	⊢ ( ∃ 𝑦 { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V )
62	1 7 60 61	4syl	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ { 𝑥 } ∈ 𝐴 } ∈ V )