This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 vsnex ⊢ { 𝑥 } ∈ 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 ⊢ 𝑋 = ∪ 𝐶