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

Metamath Proof Explorer

Theorem fgss2

Description: A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fgss2 ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ssfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
2 1 adantr ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
3 2 sseld ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑥 ∈ 𝐹 → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) )
4 ssel2 ⊢ ( ( ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) → 𝑥 ∈ ( 𝑋 filGen 𝐺 ) )
5 elfg ⊢ ( 𝐺 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐺 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) ) )
6 simpr ⊢ ( ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 )
7 5 6 biimtrdi ⊢ ( 𝐺 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐺 ) → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) )
8 7 adantl ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐺 ) → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) )
9 4 8 syl5 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) )
10 9 expd ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐹 ) → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) ) )
11 3 10 syl5d ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) → ( 𝑥 ∈ 𝐹 → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) ) )
12 11 ralrimdv ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) → ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) )
13 sseq2 ⊢ ( 𝑥 = 𝑢 → ( 𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ 𝑢 ) )
14 13 rexbidv ⊢ ( 𝑥 = 𝑢 → ( ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ↔ ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑢 ) )
15 14 rspcv ⊢ ( 𝑢 ∈ 𝐹 → ( ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑢 ) )
16 15 adantl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 → ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑢 ) )
17 sstr ⊢ ( ( 𝑦 ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑡 ) → 𝑦 ⊆ 𝑡 )
18 sseq1 ⊢ ( 𝑣 = 𝑦 → ( 𝑣 ⊆ 𝑡 ↔ 𝑦 ⊆ 𝑡 ) )
19 18 rspcev ⊢ ( ( 𝑦 ∈ 𝐺 ∧ 𝑦 ⊆ 𝑡 ) → ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 )
20 19 adantl ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ ( 𝑦 ∈ 𝐺 ∧ 𝑦 ⊆ 𝑡 ) ) → ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 )
21 20 a1d ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ ( 𝑦 ∈ 𝐺 ∧ 𝑦 ⊆ 𝑡 ) ) → ( 𝑡 ⊆ 𝑋 → ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) )
22 17 21 sylanr2 ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ ( 𝑦 ∈ 𝐺 ∧ ( 𝑦 ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑡 ) ) ) → ( 𝑡 ⊆ 𝑋 → ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) )
23 22 ancld ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ ( 𝑦 ∈ 𝐺 ∧ ( 𝑦 ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑡 ) ) ) → ( 𝑡 ⊆ 𝑋 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) )
24 23 exp45 ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) → ( 𝑦 ∈ 𝐺 → ( 𝑦 ⊆ 𝑢 → ( 𝑢 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) ) ) ) )
25 24 rexlimdv ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) → ( ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑢 → ( 𝑢 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) ) ) )
26 16 25 syld ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 → ( 𝑢 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) ) ) )
27 26 impancom ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ( 𝑢 ∈ 𝐹 → ( 𝑢 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) ) ) )
28 27 rexlimdv ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ( ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) ) )
29 28 impcomd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑡 ) → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) )
30 elfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑡 ) ) )
31 30 adantr ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑡 ) ) )
32 31 adantr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑡 ) ) )
33 elfg ⊢ ( 𝐺 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐺 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) )
34 33 adantl ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐺 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) )
35 34 adantr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐺 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐺 𝑣 ⊆ 𝑡 ) ) )
36 29 32 35 3imtr4d ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) → 𝑡 ∈ ( 𝑋 filGen 𝐺 ) ) )
37 36 ssrdv ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) → ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) )
38 37 ex ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 → ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) ) )
39 12 38 impbid ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐹 ) ⊆ ( 𝑋 filGen 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐹 ∃ 𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥 ) )