Metamath Proof Explorer

Theorem fnemeet2

Description: The meet of equivalence classes under the fineness relation-part two. (Contributed by Jeff Hankins, 6-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion fnemeet2 ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ↔ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 riin0 ⊢ ( 𝑆 = ∅ → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) = 𝒫 𝑋 )
2 1 unieqd ⊢ ( 𝑆 = ∅ → ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) = ∪ 𝒫 𝑋 )
3 unipw ⊢ ∪ 𝒫 𝑋 = 𝑋
4 2 3 eqtr2di ⊢ ( 𝑆 = ∅ → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
5 4 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑆 = ∅ → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
6 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
7 unieq ⊢ ( 𝑦 = 𝑥 → ∪ 𝑦 = ∪ 𝑥 )
8 7 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑥 ) )
9 8 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 = ∪ 𝑥 )
10 9 3adant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 = ∪ 𝑥 )
11 fnemeet1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) Fne 𝑥 )
12 eqid ⊢ ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) )
13 eqid ⊢ ∪ 𝑥 = ∪ 𝑥
14 12 13 fnebas ⊢ ( ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) Fne 𝑥 → ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) = ∪ 𝑥 )
15 11 14 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) = ∪ 𝑥 )
16 10 15 eqtr4d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
17 16 3expia ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑥 ∈ 𝑆 → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
18 17 exlimdv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( ∃ 𝑥 𝑥 ∈ 𝑆 → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
19 6 18 syl5bi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑆 ≠ ∅ → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
20 5 19 pm2.61dne ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
21 20 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
22 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
23 22 12 fnebas ⊢ ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) → ∪ 𝑇 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
24 23 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) → ∪ 𝑇 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
25 21 24 eqtr4d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) → 𝑋 = ∪ 𝑇 )
26 25 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) → 𝑋 = ∪ 𝑇 ) )
27 fnetr ⊢ ( ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ∧ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) Fne 𝑥 ) → 𝑇 Fne 𝑥 )
28 27 expcom ⊢ ( ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) Fne 𝑥 → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) → 𝑇 Fne 𝑥 ) )
29 11 28 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) → 𝑇 Fne 𝑥 ) )
30 29 3expa ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) → 𝑇 Fne 𝑥 ) )
31 30 ralrimdva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) → ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) )
32 26 31 jcad ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) → ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) )
33 simprl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → 𝑋 = ∪ 𝑇 )
34 20 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → 𝑋 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
35 33 34 eqtr3d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → ∪ 𝑇 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
36 eqimss2 ⊢ ( 𝑋 = ∪ 𝑇 → ∪ 𝑇 ⊆ 𝑋 )
37 36 ad2antrl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → ∪ 𝑇 ⊆ 𝑋 )
38 sspwuni ⊢ ( 𝑇 ⊆ 𝒫 𝑋 ↔ ∪ 𝑇 ⊆ 𝑋 )
39 37 38 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → 𝑇 ⊆ 𝒫 𝑋 )
40 breq2 ⊢ ( 𝑥 = 𝑡 → ( 𝑇 Fne 𝑥 ↔ 𝑇 Fne 𝑡 ) )
41 40 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ↔ ∀ 𝑡 ∈ 𝑆 𝑇 Fne 𝑡 )
42 fnetg ⊢ ( 𝑇 Fne 𝑡 → 𝑇 ⊆ ( topGen ‘ 𝑡 ) )
43 42 ralimi ⊢ ( ∀ 𝑡 ∈ 𝑆 𝑇 Fne 𝑡 → ∀ 𝑡 ∈ 𝑆 𝑇 ⊆ ( topGen ‘ 𝑡 ) )
44 41 43 sylbi ⊢ ( ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 → ∀ 𝑡 ∈ 𝑆 𝑇 ⊆ ( topGen ‘ 𝑡 ) )
45 44 ad2antll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → ∀ 𝑡 ∈ 𝑆 𝑇 ⊆ ( topGen ‘ 𝑡 ) )
46 ssiin ⊢ ( 𝑇 ⊆ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝑆 𝑇 ⊆ ( topGen ‘ 𝑡 ) )
47 45 46 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → 𝑇 ⊆ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) )
48 39 47 ssind ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → 𝑇 ⊆ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
49 pwexg ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V )
50 inex1g ⊢ ( 𝒫 𝑋 ∈ V → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ∈ V )
51 49 50 syl ⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ∈ V )
52 51 ad2antrr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ∈ V )
53 bastg ⊢ ( ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ∈ V → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ⊆ ( topGen ‘ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
54 52 53 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ⊆ ( topGen ‘ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
55 48 54 sstrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → 𝑇 ⊆ ( topGen ‘ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
56 22 12 isfne4 ⊢ ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ↔ ( ∪ 𝑇 = ∪ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ∧ 𝑇 ⊆ ( topGen ‘ ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) ) )
57 35 55 56 sylanbrc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) → 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) )
58 57 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) → 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ) )
59 32 58 impbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑇 Fne ( 𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 ( topGen ‘ 𝑡 ) ) ↔ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑇 Fne 𝑥 ) ) )