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

Metamath Proof Explorer

Theorem fgabs

Description: Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion fgabs ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) = ( 𝑋 filGen 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝐹 ∈ ( fBas ‘ 𝑌 ) )
2 fgcl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐹 ) ∈ ( Fil ‘ 𝑌 ) )
3 filfbas ⊢ ( ( 𝑌 filGen 𝐹 ) ∈ ( Fil ‘ 𝑌 ) → ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑌 ) )
4 1 2 3 3syl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑌 ) )
5 fbsspw ⊢ ( ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐹 ) ⊆ 𝒫 𝑌 )
6 4 5 syl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑌 filGen 𝐹 ) ⊆ 𝒫 𝑌 )
7 simplr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝑌 ⊆ 𝑋 )
8 7 sspwd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝒫 𝑌 ⊆ 𝒫 𝑋 )
9 6 8 sstrd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑌 filGen 𝐹 ) ⊆ 𝒫 𝑋 )
10 simpr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝑋 ∈ V )
11 fbasweak ⊢ ( ( ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑌 ) ∧ ( 𝑌 filGen 𝐹 ) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V ) → ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) )
12 4 9 10 11 syl3anc ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) )
13 elfg ⊢ ( ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝑌 filGen 𝐹 ) 𝑦 ⊆ 𝑥 ) ) )
14 12 13 syl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑥 ∈ ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝑌 filGen 𝐹 ) 𝑦 ⊆ 𝑥 ) ) )
15 1 adantr ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑌 ) )
16 elfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 ) ) )
17 15 16 syl ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 ) ) )
18 fbsspw ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → 𝐹 ⊆ 𝒫 𝑌 )
19 1 18 syl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝐹 ⊆ 𝒫 𝑌 )
20 19 8 sstrd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝐹 ⊆ 𝒫 𝑋 )
21 fbasweak ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
22 1 20 10 21 syl3anc ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
23 fgcl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
24 22 23 syl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
25 24 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ∧ 𝑦 ⊆ 𝑥 ) ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
26 ssfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
27 22 26 syl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
28 27 adantr ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
29 28 sselda ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ 𝑧 ∈ 𝐹 ) → 𝑧 ∈ ( 𝑋 filGen 𝐹 ) )
30 29 adantrr ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ) → 𝑧 ∈ ( 𝑋 filGen 𝐹 ) )
31 30 adantrr ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑧 ∈ ( 𝑋 filGen 𝐹 ) )
32 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ⊆ 𝑋 )
33 simprlr ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑧 ⊆ 𝑦 )
34 simprr ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ⊆ 𝑥 )
35 33 34 sstrd ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑧 ⊆ 𝑥 )
36 filss ⊢ ( ( ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑧 ∈ ( 𝑋 filGen 𝐹 ) ∧ 𝑥 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑥 ) ) → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) )
37 25 31 32 35 36 syl13anc ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) )
38 37 expr ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦 ) ) → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) )
39 38 rexlimdvaa ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) ) → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ) )
40 39 anassrs ⊢ ( ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑦 ⊆ 𝑌 ) → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ) )
41 40 expimpd ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑦 ⊆ 𝑌 ∧ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 ) → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ) )
42 17 41 sylbid ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐹 ) → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ) )
43 42 rexlimdv ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) ∧ 𝑥 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ ( 𝑌 filGen 𝐹 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) )
44 43 expimpd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ( 𝑌 filGen 𝐹 ) 𝑦 ⊆ 𝑥 ) → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) )
45 14 44 sylbid ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑥 ∈ ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) )
46 45 ssrdv ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) ⊆ ( 𝑋 filGen 𝐹 ) )
47 ssfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → 𝐹 ⊆ ( 𝑌 filGen 𝐹 ) )
48 47 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → 𝐹 ⊆ ( 𝑌 filGen 𝐹 ) )
49 fgss ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑌 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ ( 𝑌 filGen 𝐹 ) ) → ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) )
50 22 12 48 49 syl3anc ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) )
51 46 50 eqssd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) = ( 𝑋 filGen 𝐹 ) )
52 51 ex ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑋 ∈ V → ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) = ( 𝑋 filGen 𝐹 ) ) )
53 df-fg ⊢ filGen = ( 𝑤 ∈ V , 𝑥 ∈ ( fBas ‘ 𝑤 ) ↦ { 𝑦 ∈ 𝒫 𝑤 ∣ ( 𝑥 ∩ 𝒫 𝑦 ) ≠ ∅ } )
54 53 reldmmpo ⊢ Rel dom filGen
55 54 ovprc1 ⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) = ∅ )
56 54 ovprc1 ⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 filGen 𝐹 ) = ∅ )
57 55 56 eqtr4d ⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) = ( 𝑋 filGen 𝐹 ) )
58 52 57 pm2.61d1 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑋 filGen ( 𝑌 filGen 𝐹 ) ) = ( 𝑋 filGen 𝐹 ) )