Metamath Proof Explorer

Theorem fnemeet1

Description: The meet of a collection of equivalence classes of covers with respect to fineness. (Contributed by Jeff Hankins, 5-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion fnemeet1 ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) Fne 𝐴 )

Proof

Step Hyp Ref Expression
1 unitg ⊢ ( 𝑡 ∈ 𝑆 → ∪ ( topGen ‘ 𝑡 ) = ∪ 𝑡 )
2 1 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ∪ ( topGen ‘ 𝑡 ) = ∪ 𝑡 )
3 unieq ⊢ ( 𝑦 = 𝑡 → ∪ 𝑦 = ∪ 𝑡 )
4 3 eqeq2d ⊢ ( 𝑦 = 𝑡 → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑡 ) )
5 4 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑡 ∈ 𝑆 ) → 𝑋 = ∪ 𝑡 )
6 5 3ad2antl2 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → 𝑋 = ∪ 𝑡 )
7 2 6 eqtr4d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ∪ ( topGen ‘ 𝑡 ) = 𝑋 )
8 eqimss ⊢ ( ∪ ( topGen ‘ 𝑡 ) = 𝑋 → ∪ ( topGen ‘ 𝑡 ) ⊆ 𝑋 )
9 7 8 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ∪ ( topGen ‘ 𝑡 ) ⊆ 𝑋 )
10 sspwuni ⊢ ( ( topGen ‘ 𝑡 ) ⊆ 𝒫 𝑋 ↔ ∪ ( topGen ‘ 𝑡 ) ⊆ 𝑋 )
11 9 10 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ( topGen ‘ 𝑡 ) ⊆ 𝒫 𝑋 )
12 11 ralrimiva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∀ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ 𝒫 𝑋 )
13 ne0i ⊢ ( 𝐴 ∈ 𝑆 → 𝑆 ≠ ∅ )
14 13 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝑆 ≠ ∅ )
15 riinn0 ⊢ ( ( ∀ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ 𝒫 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) = ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) )
16 12 14 15 syl2anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) = ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) )
17 simp3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
18 ssid ⊢ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐴 )
19 fveq2 ⊢ ( 𝑡 = 𝐴 → ( topGen ‘ 𝑡 ) = ( topGen ‘ 𝐴 ) )
20 19 sseq1d ⊢ ( 𝑡 = 𝐴 → ( ( topGen ‘ 𝑡 ) ⊆ ( topGen ‘ 𝐴 ) ↔ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐴 ) ) )
21 20 rspcev ⊢ ( ( 𝐴 ∈ 𝑆 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐴 ) ) → ∃ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ( topGen ‘ 𝐴 ) )
22 17 18 21 sylancl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∃ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ( topGen ‘ 𝐴 ) )
23 iinss ⊢ ( ∃ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ( topGen ‘ 𝐴 ) → ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ( topGen ‘ 𝐴 ) )
24 22 23 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ( topGen ‘ 𝐴 ) )
25 24 unissd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ∪ ( topGen ‘ 𝐴 ) )
26 unitg ⊢ ( 𝐴 ∈ 𝑆 → ∪ ( topGen ‘ 𝐴 ) = ∪ 𝐴 )
27 26 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ ( topGen ‘ 𝐴 ) = ∪ 𝐴 )
28 25 27 sseqtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ∪ 𝐴 )
29 unieq ⊢ ( 𝑦 = 𝐴 → ∪ 𝑦 = ∪ 𝐴 )
30 29 eqeq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝐴 ) )
31 30 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝑋 = ∪ 𝐴 )
32 31 3adant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝑋 = ∪ 𝐴 )
33 32 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → 𝑋 = ∪ 𝐴 )
34 33 6 eqtr3d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ∪ 𝐴 = ∪ 𝑡 )
35 simpr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → 𝑡 ∈ 𝑆 )
36 ssid ⊢ 𝑡 ⊆ 𝑡
37 eltg3i ⊢ ( ( 𝑡 ∈ 𝑆 ∧ 𝑡 ⊆ 𝑡 ) → ∪ 𝑡 ∈ ( topGen ‘ 𝑡 ) )
38 35 36 37 sylancl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ∪ 𝑡 ∈ ( topGen ‘ 𝑡 ) )
39 34 38 eqeltrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ∪ 𝐴 ∈ ( topGen ‘ 𝑡 ) )
40 39 ralrimiva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∀ 𝑡 ∈ 𝑆 ∪ 𝐴 ∈ ( topGen ‘ 𝑡 ) )
41 uniexg ⊢ ( 𝐴 ∈ 𝑆 → ∪ 𝐴 ∈ V )
42 41 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝐴 ∈ V )
43 eliin ⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝑆 ∪ 𝐴 ∈ ( topGen ‘ 𝑡 ) ) )
44 42 43 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( ∪ 𝐴 ∈ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝑆 ∪ 𝐴 ∈ ( topGen ‘ 𝑡 ) ) )
45 40 44 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝐴 ∈ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) )
46 elssuni ⊢ ( ∪ 𝐴 ∈ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) → ∪ 𝐴 ⊆ ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) )
47 45 46 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝐴 ⊆ ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) )
48 28 47 eqssd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) = ∪ 𝐴 )
49 eqid ⊢ ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) = ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 )
50 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
51 49 50 isfne4 ⊢ ( ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) Fne 𝐴 ↔ ( ∪ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) = ∪ 𝐴 ∧ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ⊆ ( topGen ‘ 𝐴 ) ) )
52 48 24 51 sylanbrc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) Fne 𝐴 )
53 16 52 eqbrtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) Fne 𝐴 )