Metamath Proof Explorer

Theorem dissnref

Description: The set of singletons is a refinement of any open covering of the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020)

Ref Expression
Hypothesis dissnref.c ⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } }
Assertion dissnref ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) → 𝐶 Ref 𝑌 )

Proof

Step Hyp Ref Expression
1 dissnref.c ⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } }
2 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) → ∪ 𝑌 = 𝑋 )
3 1 unisngl ⊢ 𝑋 = ∪ 𝐶
4 2 3 eqtrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) → ∪ 𝑌 = ∪ 𝐶 )
5 simplr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑢 = { 𝑥 } )
6 simprr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑥 ∈ 𝑦 )
7 6 snssd ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦 ) ) → { 𝑥 } ⊆ 𝑦 )
8 5 7 eqsstrd ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑢 ⊆ 𝑦 )
9 simplr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → 𝑥 ∈ 𝑋 )
10 simp-4r ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → ∪ 𝑌 = 𝑋 )
11 9 10 eleqtrrd ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → 𝑥 ∈ ∪ 𝑌 )
12 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝑌 ↔ ∃ 𝑦 ∈ 𝑌 𝑥 ∈ 𝑦 )
13 11 12 sylib ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → ∃ 𝑦 ∈ 𝑌 𝑥 ∈ 𝑦 )
14 8 13 reximddv ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → ∃ 𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦 )
15 1 eqabri ⊢ ( 𝑢 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } )
16 15 bilani ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } )
17 14 16 r19.29a ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) ∧ 𝑢 ∈ 𝐶 ) → ∃ 𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦 )
18 17 ralrimiva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) → ∀ 𝑢 ∈ 𝐶 ∃ 𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦 )
19 pwexg ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V )
20 simpr ⊢ ( ( ( 𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → 𝑢 = { 𝑥 } )
21 snelpwi ⊢ ( 𝑥 ∈ 𝑋 → { 𝑥 } ∈ 𝒫 𝑋 )
22 21 ad2antlr ⊢ ( ( ( 𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → { 𝑥 } ∈ 𝒫 𝑋 )
23 20 22 eqeltrd ⊢ ( ( ( 𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝒫 𝑋 )
24 15 biimpi ⊢ ( 𝑢 ∈ 𝐶 → ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } )
25 23 24 r19.29a ⊢ ( 𝑢 ∈ 𝐶 → 𝑢 ∈ 𝒫 𝑋 )
26 25 ssriv ⊢ 𝐶 ⊆ 𝒫 𝑋
27 26 a1i ⊢ ( 𝑋 ∈ 𝑉 → 𝐶 ⊆ 𝒫 𝑋 )
28 19 27 ssexd ⊢ ( 𝑋 ∈ 𝑉 → 𝐶 ∈ V )
29 28 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) → 𝐶 ∈ V )
30 eqid ⊢ ∪ 𝐶 = ∪ 𝐶
31 eqid ⊢ ∪ 𝑌 = ∪ 𝑌
32 30 31 isref ⊢ ( 𝐶 ∈ V → ( 𝐶 Ref 𝑌 ↔ ( ∪ 𝑌 = ∪ 𝐶 ∧ ∀ 𝑢 ∈ 𝐶 ∃ 𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦 ) ) )
33 29 32 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) → ( 𝐶 Ref 𝑌 ↔ ( ∪ 𝑌 = ∪ 𝐶 ∧ ∀ 𝑢 ∈ 𝐶 ∃ 𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦 ) ) )
34 4 18 33 mpbir2and ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋 ) → 𝐶 Ref 𝑌 )