Metamath Proof Explorer

Theorem fmfnfm

Description: A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypotheses fmfnfm.b ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
Assertion fmfnfm ( 𝜑 → ∃ 𝑓 ∈ ( Fil ‘ 𝑌 ) ( 𝐵 ⊆ 𝑓 ∧ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
2 fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
3 fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
4 fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
5 fbsspw ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ 𝒫 𝑌 )
6 1 5 syl ⊢ ( 𝜑 → 𝐵 ⊆ 𝒫 𝑌 )
7 elfvdm ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ dom fBas )
8 1 7 syl ⊢ ( 𝜑 → 𝑌 ∈ dom fBas )
9 ffn ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 Fn 𝑌 )
10 dffn4 ⊢ ( 𝐹 Fn 𝑌 ↔ 𝐹 : 𝑌 –onto→ ran 𝐹 )
11 9 10 sylib ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 : 𝑌 –onto→ ran 𝐹 )
12 foima ⊢ ( 𝐹 : 𝑌 –onto→ ran 𝐹 → ( 𝐹 “ 𝑌 ) = ran 𝐹 )
13 3 11 12 3syl ⊢ ( 𝜑 → ( 𝐹 “ 𝑌 ) = ran 𝐹 )
14 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐿 )
15 2 14 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
16 fgcl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
17 filtop ⊢ ( ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ ( 𝑌 filGen 𝐵 ) )
18 1 16 17 3syl ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑌 filGen 𝐵 ) )
19 eqid ⊢ ( 𝑌 filGen 𝐵 ) = ( 𝑌 filGen 𝐵 )
20 19 imaelfm ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑌 ∈ ( 𝑌 filGen 𝐵 ) ) → ( 𝐹 “ 𝑌 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
21 15 1 3 18 20 syl31anc ⊢ ( 𝜑 → ( 𝐹 “ 𝑌 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
22 13 21 eqeltrrd ⊢ ( 𝜑 → ran 𝐹 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
23 4 22 sseldd ⊢ ( 𝜑 → ran 𝐹 ∈ 𝐿 )
24 rnelfmlem ⊢ ( ( ( 𝑌 ∈ dom fBas ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) )
25 8 2 3 23 24 syl31anc ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) )
26 fbsspw ⊢ ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝒫 𝑌 )
27 25 26 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝒫 𝑌 )
28 6 27 unssd ⊢ ( 𝜑 → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝒫 𝑌 )
29 ssun1 ⊢ 𝐵 ⊆ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
30 fbasne0 ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ≠ ∅ )
31 1 30 syl ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
32 ssn0 ⊢ ( ( 𝐵 ⊆ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∧ 𝐵 ≠ ∅ ) → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ≠ ∅ )
33 29 31 32 sylancr ⊢ ( 𝜑 → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ≠ ∅ )
34 eqid ⊢ ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) )
35 34 elrnmpt ⊢ ( 𝑡 ∈ V → ( 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) ) )
36 35 elv ⊢ ( 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) )
37 0nelfil ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐿 )
38 2 37 syl ⊢ ( 𝜑 → ¬ ∅ ∈ 𝐿 )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ¬ ∅ ∈ 𝐿 )
40 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
41 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
42 15 1 3 3jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) )
44 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) )
45 1 44 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) )
46 45 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ∈ ( 𝑌 filGen 𝐵 ) )
47 19 imaelfm ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑠 ∈ ( 𝑌 filGen 𝐵 ) ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
48 43 46 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
49 41 48 sseldd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝐹 “ 𝑠 ) ∈ 𝐿 )
50 40 49 jca ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) )
51 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 )
52 51 3expa ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 )
53 50 52 sylan ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 )
54 eleq1 ⊢ ( ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) = ∅ → ( ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 ↔ ∅ ∈ 𝐿 ) )
55 53 54 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) = ∅ → ∅ ∈ 𝐿 ) )
56 39 55 mtod ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ¬ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) = ∅ )
57 neq0 ⊢ ( ¬ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) = ∅ ↔ ∃ 𝑡 𝑡 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) )
58 elin ⊢ ( 𝑡 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ↔ ( 𝑡 ∈ ( 𝐹 “ 𝑠 ) ∧ 𝑡 ∈ 𝑥 ) )
59 ffun ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → Fun 𝐹 )
60 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑡 ∈ ( 𝐹 “ 𝑠 ) ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑡 )
61 60 ex ⊢ ( Fun 𝐹 → ( 𝑡 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑡 ) )
62 3 59 61 3syl ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑡 ) )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑡 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑡 ) )
64 3 59 syl ⊢ ( 𝜑 → Fun 𝐹 )
65 64 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑦 ∈ 𝑠 ) → Fun 𝐹 )
66 fbelss ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ 𝑌 )
67 1 66 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ 𝑌 )
68 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑌 )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → dom 𝐹 = 𝑌 )
70 67 69 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ dom 𝐹 )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → 𝑠 ⊆ dom 𝐹 )
72 71 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ dom 𝐹 )
73 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
74 65 72 73 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
75 inelcm ⊢ ( ( 𝑦 ∈ 𝑠 ∧ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ )
76 75 ex ⊢ ( 𝑦 ∈ 𝑠 → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
77 76 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
78 74 77 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
79 eleq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑡 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑡 ∈ 𝑥 ) )
80 79 imbi1d ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑡 → ( ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) ↔ ( 𝑡 ∈ 𝑥 → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) ) )
81 78 80 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑡 → ( 𝑡 ∈ 𝑥 → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) ) )
82 81 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑡 → ( 𝑡 ∈ 𝑥 → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) ) )
83 63 82 syld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑡 ∈ ( 𝐹 “ 𝑠 ) → ( 𝑡 ∈ 𝑥 → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) ) )
84 83 impd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝑡 ∈ ( 𝐹 “ 𝑠 ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
85 58 84 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑡 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
86 85 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ∃ 𝑡 𝑡 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
87 57 86 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ¬ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) = ∅ → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
88 56 87 mpd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ )
89 ineq2 ⊢ ( 𝑡 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝑠 ∩ 𝑡 ) = ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) )
90 89 neeq1d ⊢ ( 𝑡 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝑠 ∩ 𝑡 ) ≠ ∅ ↔ ( 𝑠 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
91 88 90 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑡 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
92 91 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
93 36 92 biimtrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
94 93 expimpd ⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
95 94 ralrimivv ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝑠 ∩ 𝑡 ) ≠ ∅ )
96 fbunfip ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
97 1 25 96 syl2anc ⊢ ( 𝜑 → ( ¬ ∅ ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
98 95 97 mpbird ⊢ ( 𝜑 → ¬ ∅ ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
99 fsubbas ⊢ ( 𝑌 ∈ dom fBas → ( ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∈ ( fBas ‘ 𝑌 ) ↔ ( ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝒫 𝑌 ∧ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
100 1 7 99 3syl ⊢ ( 𝜑 → ( ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∈ ( fBas ‘ 𝑌 ) ↔ ( ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝒫 𝑌 ∧ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
101 28 33 98 100 mpbir3and ⊢ ( 𝜑 → ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∈ ( fBas ‘ 𝑌 ) )
102 fgcl ⊢ ( ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ∈ ( Fil ‘ 𝑌 ) )
103 101 102 syl ⊢ ( 𝜑 → ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ∈ ( Fil ‘ 𝑌 ) )
104 unexg ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) ) → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V )
105 1 25 104 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V )
106 ssfii ⊢ ( ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
107 105 106 syl ⊢ ( 𝜑 → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
108 107 unssad ⊢ ( 𝜑 → 𝐵 ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
109 ssfg ⊢ ( ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∈ ( fBas ‘ 𝑌 ) → ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ⊆ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
110 101 109 syl ⊢ ( 𝜑 → ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ⊆ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
111 108 110 sstrd ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
112 1 2 3 4 fmfnfmlem4 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
113 elfm ⊢ ( ( 𝑋 ∈ 𝐿 ∧ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
114 15 101 3 113 syl3anc ⊢ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
115 112 114 bitr4d ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
116 115 eqrdv ⊢ ( 𝜑 → 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
117 eqid ⊢ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) = ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
118 117 fmfg ⊢ ( ( 𝑋 ∈ 𝐿 ∧ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) = ( ( 𝑋 FilMap 𝐹 ) ‘ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
119 15 101 3 118 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) = ( ( 𝑋 FilMap 𝐹 ) ‘ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
120 116 119 eqtrd ⊢ ( 𝜑 → 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
121 sseq2 ⊢ ( 𝑓 = ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( 𝐵 ⊆ 𝑓 ↔ 𝐵 ⊆ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
122 fveq2 ⊢ ( 𝑓 = ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑓 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) )
123 122 eqeq2d ⊢ ( 𝑓 = ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑓 ) ↔ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) ) )
124 121 123 anbi12d ⊢ ( 𝑓 = ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( ( 𝐵 ⊆ 𝑓 ∧ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑓 ) ) ↔ ( 𝐵 ⊆ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ∧ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) ) ) )
125 124 rspcev ⊢ ( ( ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐵 ⊆ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ∧ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ( 𝑌 filGen ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑌 ) ( 𝐵 ⊆ 𝑓 ∧ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑓 ) ) )
126 103 111 120 125 syl12anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( Fil ‘ 𝑌 ) ( 𝐵 ⊆ 𝑓 ∧ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑓 ) ) )