Metamath Proof Explorer

Theorem trufil

Description: Conditions for the trace of an ultrafilter L to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion trufil ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( UFil ‘ 𝐴 ) ↔ 𝐴 ∈ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 ufilfil ⊢ ( ( 𝐿 ↾t 𝐴 ) ∈ ( UFil ‘ 𝐴 ) → ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
2 ufilfil ⊢ ( 𝐿 ∈ ( UFil ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
3 trfil3 ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
4 2 3 sylan ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
5 1 4 syl5ib ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( UFil ‘ 𝐴 ) → ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
6 4 biimprd ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 → ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
7 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
8 simpll ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → 𝐿 ∈ ( UFil ‘ 𝑌 ) )
9 simpr ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐴 )
10 simplr ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → 𝐴 ⊆ 𝑌 )
11 9 10 sstrd ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝑌 )
12 ufilss ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( 𝑥 ∈ 𝐿 ∨ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) )
13 8 11 12 syl2anc ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝐿 ∨ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) )
14 id ⊢ ( 𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌 )
15 elfvdm ⊢ ( 𝐿 ∈ ( UFil ‘ 𝑌 ) → 𝑌 ∈ dom UFil )
16 ssexg ⊢ ( ( 𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ dom UFil ) → 𝐴 ∈ V )
17 14 15 16 syl2anr ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
18 elrestr ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ 𝑥 ∈ 𝐿 ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
19 18 3expia ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ 𝐿 → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
20 17 19 syldan ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑥 ∈ 𝐿 → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
21 20 adantr ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝐿 → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
22 df-ss ⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) = 𝑥 )
23 9 22 sylib ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ∩ 𝐴 ) = 𝑥 )
24 23 eleq1d ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) ↔ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) )
25 21 24 sylibd ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝐿 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) )
26 indif1 ⊢ ( ( 𝑌 ∖ 𝑥 ) ∩ 𝐴 ) = ( ( 𝑌 ∩ 𝐴 ) ∖ 𝑥 )
27 simplr ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → 𝐴 ⊆ 𝑌 )
28 sseqin2 ⊢ ( 𝐴 ⊆ 𝑌 ↔ ( 𝑌 ∩ 𝐴 ) = 𝐴 )
29 27 28 sylib ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → ( 𝑌 ∩ 𝐴 ) = 𝐴 )
30 29 difeq1d ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → ( ( 𝑌 ∩ 𝐴 ) ∖ 𝑥 ) = ( 𝐴 ∖ 𝑥 ) )
31 26 30 syl5eq ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → ( ( 𝑌 ∖ 𝑥 ) ∩ 𝐴 ) = ( 𝐴 ∖ 𝑥 ) )
32 simpll ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → 𝐿 ∈ ( UFil ‘ 𝑌 ) )
33 17 adantr ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → 𝐴 ∈ V )
34 simprr ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 )
35 elrestr ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) → ( ( 𝑌 ∖ 𝑥 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
36 32 33 34 35 syl3anc ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → ( ( 𝑌 ∖ 𝑥 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
37 31 36 eqeltrrd ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) ) → ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) )
38 37 expr ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 → ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
39 25 38 orim12d ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑥 ∈ 𝐿 ∨ ( 𝑌 ∖ 𝑥 ) ∈ 𝐿 ) → ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∨ ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) )
40 13 39 mpd ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∨ ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
41 7 40 sylan2 ⊢ ( ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∨ ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
42 41 ralrimiva ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∨ ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
43 6 42 jctird ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∨ ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) ) )
44 isufil ⊢ ( ( 𝐿 ↾t 𝐴 ) ∈ ( UFil ‘ 𝐴 ) ↔ ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∨ ( 𝐴 ∖ 𝑥 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) )
45 43 44 syl6ibr ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 → ( 𝐿 ↾t 𝐴 ) ∈ ( UFil ‘ 𝐴 ) ) )
46 5 45 impbid ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( UFil ‘ 𝐴 ) ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
47 ufilb ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ 𝐴 ∈ 𝐿 ↔ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
48 47 con1bid ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ↔ 𝐴 ∈ 𝐿 ) )
49 46 48 bitrd ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( UFil ‘ 𝐴 ) ↔ 𝐴 ∈ 𝐿 ) )