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 ⊢ L ∈ UFil ⁡ Y ∧ A ⊆ Y → L ↾ 𝑡 A ∈ UFil ⁡ A ↔ A ∈ L

Proof

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