Theorem unisngl

Description: Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020)

	Ref	Expression
Hypothesis	dissnref.c	⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } }
Assertion	unisngl	⊢ 𝑋 = ∪ 𝐶

Proof

Step	Hyp	Ref	Expression
1		dissnref.c	⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } }
2	1	unieqi	⊢ ∪ 𝐶 = ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } }
3		simpl	⊢ ( ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) → 𝑦 ∈ 𝑢 )
4		simpr	⊢ ( ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) → 𝑢 = { 𝑥 } )
5	3 4	eleqtrd	⊢ ( ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) → 𝑦 ∈ { 𝑥 } )
6	5	exlimiv	⊢ ( ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) → 𝑦 ∈ { 𝑥 } )
7		eqid	⊢ { 𝑥 } = { 𝑥 }
8		snex	⊢ { 𝑥 } ∈ V
9		eleq2	⊢ ( 𝑢 = { 𝑥 } → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ { 𝑥 } ) )
10		eqeq1	⊢ ( 𝑢 = { 𝑥 } → ( 𝑢 = { 𝑥 } ↔ { 𝑥 } = { 𝑥 } ) )
11	9 10	anbi12d	⊢ ( 𝑢 = { 𝑥 } → ( ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) ↔ ( 𝑦 ∈ { 𝑥 } ∧ { 𝑥 } = { 𝑥 } ) ) )
12	8 11	spcev	⊢ ( ( 𝑦 ∈ { 𝑥 } ∧ { 𝑥 } = { 𝑥 } ) → ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) )
13	7 12	mpan2	⊢ ( 𝑦 ∈ { 𝑥 } → ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) )
14	6 13	impbii	⊢ ( ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) ↔ 𝑦 ∈ { 𝑥 } )
15		velsn	⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
16		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
17	14 15 16	3bitri	⊢ ( ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) ↔ 𝑥 = 𝑦 )
18	17	rexbii	⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑋 𝑥 = 𝑦 )
19		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝑋 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) ↔ ( 𝑦 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ) )
20	19	exbii	⊢ ( ∃ 𝑢 ∃ 𝑥 ∈ 𝑋 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) ↔ ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ) )
21		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) ↔ ∃ 𝑢 ∃ 𝑥 ∈ 𝑋 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) )
22		eluniab	⊢ ( 𝑦 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ↔ ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ) )
23	20 21 22	3bitr4ri	⊢ ( 𝑦 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ 𝑢 = { 𝑥 } ) )
24		risset	⊢ ( 𝑦 ∈ 𝑋 ↔ ∃ 𝑥 ∈ 𝑋 𝑥 = 𝑦 )
25	18 23 24	3bitr4i	⊢ ( 𝑦 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ↔ 𝑦 ∈ 𝑋 )
26	25	eqriv	⊢ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } = 𝑋
27	2 26	eqtr2i	⊢ 𝑋 = ∪ 𝐶