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