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 ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝐴 ) → 𝐹 ∈ ( fBas ‘ 𝐴 ) )
2 1 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ ( fBas ‘ 𝐴 ) )
3 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝐴 ) → 𝐹 ⊆ 𝒫 𝐴 )
4 3 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ⊆ 𝒫 𝐴 )
5 simp2 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐴 ⊆ 𝑋 )
6 5 sspwd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝒫 𝐴 ⊆ 𝒫 𝑋 )
7 4 6 sstrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ⊆ 𝒫 𝑋 )
8 simp3 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
9 fbasweak ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐴 ) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
10 2 7 8 9 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
11 fgcl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
12 10 11 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
13 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝐴 ) → 𝐴 ∈ 𝐹 )
14 13 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐴 ∈ 𝐹 )
15 restval ⊢ ( ( ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) = ran ( 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ↦ ( 𝑥 ∩ 𝐴 ) ) )
16 12 14 15 syl2anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) = ran ( 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ↦ ( 𝑥 ∩ 𝐴 ) ) )
17 elfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 ) ) )
18 10 17 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 ) ) )
19 18 simplbda ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 )
20 simpll1 ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝐹 ∈ ( Fil ‘ 𝐴 ) )
21 simprl ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ 𝐹 )
22 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
23 22 a1i ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
24 simprr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ⊆ 𝑥 )
25 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝐴 )
26 25 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝐴 )
27 26 ad2ant2r ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ⊆ 𝐴 )
28 24 27 ssind ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ⊆ ( 𝑥 ∩ 𝐴 ) )
29 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ ( 𝑦 ∈ 𝐹 ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ∧ 𝑦 ⊆ ( 𝑥 ∩ 𝐴 ) ) ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝐹 )
30 20 21 23 28 29 syl13anc ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝐹 )
31 19 30 rexlimddv ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝐹 )
32 31 fmpttd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ↦ ( 𝑥 ∩ 𝐴 ) ) : ( 𝑋 filGen 𝐹 ) ⟶ 𝐹 )
33 32 frnd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ran ( 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ↦ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝐹 )
34 16 33 eqsstrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) ⊆ 𝐹 )
35 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ 𝐴 )
36 35 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ 𝐴 )
37 dfss2 ⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) = 𝑥 )
38 36 37 sylib ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) = 𝑥 )
39 12 adantr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
40 14 adantr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐹 ) → 𝐴 ∈ 𝐹 )
41 ssfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
42 10 41 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
43 42 sselda ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ ( 𝑋 filGen 𝐹 ) )
44 elrestr ⊢ ( ( ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝑋 filGen 𝐹 ) ) → ( 𝑥 ∩ 𝐴 ) ∈ ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) )
45 39 40 43 44 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) )
46 38 45 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) )
47 34 46 eqelssd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑋 filGen 𝐹 ) ↾t 𝐴 ) = 𝐹 )