Metamath Proof Explorer

Theorem ssufl

Description: If Y is a subset of X and filters extend to ultrafilters in X , then they still do in Y . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ssufl ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ UFL )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝑋 ∈ UFL )
2 filfbas ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑌 ) → 𝑓 ∈ ( fBas ‘ 𝑌 ) )
3 2 adantl ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝑓 ∈ ( fBas ‘ 𝑌 ) )
4 filsspw ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑌 ) → 𝑓 ⊆ 𝒫 𝑌 )
5 4 adantl ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝑓 ⊆ 𝒫 𝑌 )
6 simplr ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
7 6 sspwd ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝒫 𝑌 ⊆ 𝒫 𝑋 )
8 5 7 sstrd ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝑓 ⊆ 𝒫 𝑋 )
9 fbasweak ⊢ ( ( 𝑓 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑓 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ UFL ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
10 3 8 1 9 syl3anc ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
11 fgcl ⊢ ( 𝑓 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝑓 ) ∈ ( Fil ‘ 𝑋 ) )
12 10 11 syl ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑋 filGen 𝑓 ) ∈ ( Fil ‘ 𝑋 ) )
13 ufli ⊢ ( ( 𝑋 ∈ UFL ∧ ( 𝑋 filGen 𝑓 ) ∈ ( Fil ‘ 𝑋 ) ) → ∃ 𝑢 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 )
14 1 12 13 syl2anc ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → ∃ 𝑢 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 )
15 ssfg ⊢ ( 𝑓 ∈ ( fBas ‘ 𝑋 ) → 𝑓 ⊆ ( 𝑋 filGen 𝑓 ) )
16 10 15 syl ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → 𝑓 ⊆ ( 𝑋 filGen 𝑓 ) )
17 16 adantr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑓 ⊆ ( 𝑋 filGen 𝑓 ) )
18 simprr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 )
19 17 18 sstrd ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑓 ⊆ 𝑢 )
20 filtop ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ 𝑓 )
21 20 ad2antlr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑌 ∈ 𝑓 )
22 19 21 sseldd ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑌 ∈ 𝑢 )
23 simprl ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑢 ∈ ( UFil ‘ 𝑋 ) )
24 6 adantr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑌 ⊆ 𝑋 )
25 trufil ⊢ ( ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ( 𝑢 ↾t 𝑌 ) ∈ ( UFil ‘ 𝑌 ) ↔ 𝑌 ∈ 𝑢 ) )
26 23 24 25 syl2anc ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → ( ( 𝑢 ↾t 𝑌 ) ∈ ( UFil ‘ 𝑌 ) ↔ 𝑌 ∈ 𝑢 ) )
27 22 26 mpbird ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → ( 𝑢 ↾t 𝑌 ) ∈ ( UFil ‘ 𝑌 ) )
28 5 adantr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑓 ⊆ 𝒫 𝑌 )
29 restid2 ⊢ ( ( 𝑌 ∈ 𝑓 ∧ 𝑓 ⊆ 𝒫 𝑌 ) → ( 𝑓 ↾t 𝑌 ) = 𝑓 )
30 21 28 29 syl2anc ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → ( 𝑓 ↾t 𝑌 ) = 𝑓 )
31 ssrest ⊢ ( ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ⊆ 𝑢 ) → ( 𝑓 ↾t 𝑌 ) ⊆ ( 𝑢 ↾t 𝑌 ) )
32 23 19 31 syl2anc ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → ( 𝑓 ↾t 𝑌 ) ⊆ ( 𝑢 ↾t 𝑌 ) )
33 30 32 eqsstrrd ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → 𝑓 ⊆ ( 𝑢 ↾t 𝑌 ) )
34 sseq2 ⊢ ( 𝑔 = ( 𝑢 ↾t 𝑌 ) → ( 𝑓 ⊆ 𝑔 ↔ 𝑓 ⊆ ( 𝑢 ↾t 𝑌 ) ) )
35 34 rspcev ⊢ ( ( ( 𝑢 ↾t 𝑌 ) ∈ ( UFil ‘ 𝑌 ) ∧ 𝑓 ⊆ ( 𝑢 ↾t 𝑌 ) ) → ∃ 𝑔 ∈ ( UFil ‘ 𝑌 ) 𝑓 ⊆ 𝑔 )
36 27 33 35 syl2anc ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑢 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ⊆ 𝑢 ) ) → ∃ 𝑔 ∈ ( UFil ‘ 𝑌 ) 𝑓 ⊆ 𝑔 )
37 14 36 rexlimddv ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑌 ) ) → ∃ 𝑔 ∈ ( UFil ‘ 𝑌 ) 𝑓 ⊆ 𝑔 )
38 37 ralrimiva ⊢ ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑌 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑌 ) 𝑓 ⊆ 𝑔 )
39 ssexg ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ UFL ) → 𝑌 ∈ V )
40 39 ancoms ⊢ ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ V )
41 isufl ⊢ ( 𝑌 ∈ V → ( 𝑌 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑌 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑌 ) 𝑓 ⊆ 𝑔 ) )
42 40 41 syl ⊢ ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑌 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑌 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑌 ) 𝑓 ⊆ 𝑔 ) )
43 38 42 mpbird ⊢ ( ( 𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ UFL )