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 e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( UFil ` A ) <-> A e. L ) )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( ( L |`t A ) e. ( UFil ` A ) -> ( L |`t A ) e. ( Fil ` A ) )
2 ufilfil 
 |-  ( L e. ( UFil ` Y ) -> L e. ( Fil ` Y ) )
3 trfil3 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> -. ( Y \ A ) e. L ) )
4 2 3 sylan 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> -. ( Y \ A ) e. L ) )
5 1 4 imbitrid 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( UFil ` A ) -> -. ( Y \ A ) e. L ) )
6 4 biimprd 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L -> ( L |`t A ) e. ( Fil ` A ) ) )
7 elpwi 
 |-  ( x e. ~P A -> x C_ A )
8 simpll 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> L e. ( UFil ` Y ) )
9 simpr 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> x C_ A )
10 simplr 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> A C_ Y )
11 9 10 sstrd 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> x C_ Y )
12 ufilss 
 |-  ( ( L e. ( UFil ` Y ) /\ x C_ Y ) -> ( x e. L \/ ( Y \ x ) e. L ) )
13 8 11 12 syl2anc 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. L \/ ( Y \ x ) e. L ) )
14 id 
 |-  ( A C_ Y -> A C_ Y )
15 elfvdm 
 |-  ( L e. ( UFil ` Y ) -> Y e. dom UFil )
16 ssexg 
 |-  ( ( A C_ Y /\ Y e. dom UFil ) -> A e. _V )
17 14 15 16 syl2anr 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> A e. _V )
18 elrestr 
 |-  ( ( L e. ( UFil ` Y ) /\ A e. _V /\ x e. L ) -> ( x i^i A ) e. ( L |`t A ) )
19 18 3expia 
 |-  ( ( L e. ( UFil ` Y ) /\ A e. _V ) -> ( x e. L -> ( x i^i A ) e. ( L |`t A ) ) )
20 17 19 syldan 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( x e. L -> ( x i^i A ) e. ( L |`t A ) ) )
21 20 adantr 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. L -> ( x i^i A ) e. ( L |`t A ) ) )
22 dfss2 
 |-  ( x C_ A <-> ( x i^i A ) = x )
23 9 22 sylib 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x i^i A ) = x )
24 23 eleq1d 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( ( x i^i A ) e. ( L |`t A ) <-> x e. ( L |`t A ) ) )
25 21 24 sylibd 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. L -> x e. ( L |`t A ) ) )
26 indif1 
 |-  ( ( Y \ x ) i^i A ) = ( ( Y i^i A ) \ x )
27 simplr 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> A C_ Y )
28 sseqin2 
 |-  ( A C_ Y <-> ( Y i^i A ) = A )
29 27 28 sylib 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( Y i^i A ) = A )
30 29 difeq1d 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( ( Y i^i A ) \ x ) = ( A \ x ) )
31 26 30 eqtrid 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( ( Y \ x ) i^i A ) = ( A \ x ) )
32 simpll 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> L e. ( UFil ` Y ) )
33 17 adantr 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> A e. _V )
34 simprr 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( Y \ x ) e. L )
35 elrestr 
 |-  ( ( L e. ( UFil ` Y ) /\ A e. _V /\ ( Y \ x ) e. L ) -> ( ( Y \ x ) i^i A ) e. ( L |`t A ) )
36 32 33 34 35 syl3anc 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( ( Y \ x ) i^i A ) e. ( L |`t A ) )
37 31 36 eqeltrrd 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ ( x C_ A /\ ( Y \ x ) e. L ) ) -> ( A \ x ) e. ( L |`t A ) )
38 37 expr 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( ( Y \ x ) e. L -> ( A \ x ) e. ( L |`t A ) ) )
39 25 38 orim12d 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( ( x e. L \/ ( Y \ x ) e. L ) -> ( x e. ( L |`t A ) \/ ( A \ x ) e. ( L |`t A ) ) ) )
40 13 39 mpd 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( x e. ( L |`t A ) \/ ( A \ x ) e. ( L |`t A ) ) )
41 7 40 sylan2 
 |-  ( ( ( L e. ( UFil ` Y ) /\ A C_ Y ) /\ x e. ~P A ) -> ( x e. ( L |`t A ) \/ ( A \ x ) e. ( L |`t A ) ) )
42 41 ralrimiva 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> A. x e. ~P A ( x e. ( L |`t A ) \/ ( A \ x ) e. ( L |`t A ) ) )
43 6 42 jctird 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L -> ( ( L |`t A ) e. ( Fil ` A ) /\ A. x e. ~P A ( x e. ( L |`t A ) \/ ( A \ x ) e. ( L |`t A ) ) ) ) )
44 isufil 
 |-  ( ( L |`t A ) e. ( UFil ` A ) <-> ( ( L |`t A ) e. ( Fil ` A ) /\ A. x e. ~P A ( x e. ( L |`t A ) \/ ( A \ x ) e. ( L |`t A ) ) ) )
45 43 44 imbitrrdi 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L -> ( L |`t A ) e. ( UFil ` A ) ) )
46 5 45 impbid 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( UFil ` A ) <-> -. ( Y \ A ) e. L ) )
47 ufilb 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. A e. L <-> ( Y \ A ) e. L ) )
48 47 con1bid 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( -. ( Y \ A ) e. L <-> A e. L ) )
49 46 48 bitrd 
 |-  ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( UFil ` A ) <-> A e. L ) )