Metamath Proof Explorer

Theorem trfg

Description: The trace operation and the filGen operation are inverses to one another in some sense, with filGen growing the base set and ` |``t ` shrinking it. See fgtr for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion trfg 
|- ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( ( X filGen F ) |`t A ) = F )

Proof

Step Hyp Ref Expression
1 filfbas 
 |-  ( F e. ( Fil ` A ) -> F e. ( fBas ` A ) )
2 1 3ad2ant1 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> F e. ( fBas ` A ) )
3 filsspw 
 |-  ( F e. ( Fil ` A ) -> F C_ ~P A )
4 3 3ad2ant1 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> F C_ ~P A )
5 simp2 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> A C_ X )
6 5 sspwd 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ~P A C_ ~P X )
7 4 6 sstrd 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> F C_ ~P X )
8 simp3 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> X e. V )
9 fbasweak 
 |-  ( ( F e. ( fBas ` A ) /\ F C_ ~P X /\ X e. V ) -> F e. ( fBas ` X ) )
10 2 7 8 9 syl3anc 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> F e. ( fBas ` X ) )
11 fgcl 
 |-  ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )
12 10 11 syl 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( X filGen F ) e. ( Fil ` X ) )
13 filtop 
 |-  ( F e. ( Fil ` A ) -> A e. F )
14 13 3ad2ant1 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> A e. F )
15 restval 
 |-  ( ( ( X filGen F ) e. ( Fil ` X ) /\ A e. F ) -> ( ( X filGen F ) |`t A ) = ran ( x e. ( X filGen F ) |-> ( x i^i A ) ) )
16 12 14 15 syl2anc 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( ( X filGen F ) |`t A ) = ran ( x e. ( X filGen F ) |-> ( x i^i A ) ) )
17 elfg 
 |-  ( F e. ( fBas ` X ) -> ( x e. ( X filGen F ) <-> ( x C_ X /\ E. y e. F y C_ x ) ) )
18 10 17 syl 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( x e. ( X filGen F ) <-> ( x C_ X /\ E. y e. F y C_ x ) ) )
19 18 simplbda 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) -> E. y e. F y C_ x )
20 simpll1 
 |-  ( ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) /\ ( y e. F /\ y C_ x ) ) -> F e. ( Fil ` A ) )
21 simprl 
 |-  ( ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) /\ ( y e. F /\ y C_ x ) ) -> y e. F )
22 inss2 
 |-  ( x i^i A ) C_ A
23 22 a1i 
 |-  ( ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) /\ ( y e. F /\ y C_ x ) ) -> ( x i^i A ) C_ A )
24 simprr 
 |-  ( ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) /\ ( y e. F /\ y C_ x ) ) -> y C_ x )
25 filelss 
 |-  ( ( F e. ( Fil ` A ) /\ y e. F ) -> y C_ A )
26 25 3ad2antl1 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ y e. F ) -> y C_ A )
27 26 ad2ant2r 
 |-  ( ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) /\ ( y e. F /\ y C_ x ) ) -> y C_ A )
28 24 27 ssind 
 |-  ( ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) /\ ( y e. F /\ y C_ x ) ) -> y C_ ( x i^i A ) )
29 filss 
 |-  ( ( F e. ( Fil ` A ) /\ ( y e. F /\ ( x i^i A ) C_ A /\ y C_ ( x i^i A ) ) ) -> ( x i^i A ) e. F )
30 20 21 23 28 29 syl13anc 
 |-  ( ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) /\ ( y e. F /\ y C_ x ) ) -> ( x i^i A ) e. F )
31 19 30 rexlimddv 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. ( X filGen F ) ) -> ( x i^i A ) e. F )
32 31 fmpttd 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( x e. ( X filGen F ) |-> ( x i^i A ) ) : ( X filGen F ) --> F )
33 32 frnd 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ran ( x e. ( X filGen F ) |-> ( x i^i A ) ) C_ F )
34 16 33 eqsstrd 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( ( X filGen F ) |`t A ) C_ F )
35 filelss 
 |-  ( ( F e. ( Fil ` A ) /\ x e. F ) -> x C_ A )
36 35 3ad2antl1 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. F ) -> x C_ A )
37 df-ss 
 |-  ( x C_ A <-> ( x i^i A ) = x )
38 36 37 sylib 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. F ) -> ( x i^i A ) = x )
39 12 adantr 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. F ) -> ( X filGen F ) e. ( Fil ` X ) )
40 14 adantr 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. F ) -> A e. F )
41 ssfg 
 |-  ( F e. ( fBas ` X ) -> F C_ ( X filGen F ) )
42 10 41 syl 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> F C_ ( X filGen F ) )
43 42 sselda 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. F ) -> x e. ( X filGen F ) )
44 elrestr 
 |-  ( ( ( X filGen F ) e. ( Fil ` X ) /\ A e. F /\ x e. ( X filGen F ) ) -> ( x i^i A ) e. ( ( X filGen F ) |`t A ) )
45 39 40 43 44 syl3anc 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. F ) -> ( x i^i A ) e. ( ( X filGen F ) |`t A ) )
46 38 45 eqeltrrd 
 |-  ( ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) /\ x e. F ) -> x e. ( ( X filGen F ) |`t A ) )
47 34 46 eqelssd 
 |-  ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( ( X filGen F ) |`t A ) = F )