This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnelfm

Description: A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion rnelfm ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐿 ∈ ran ( 𝑋 FilMap 𝐹 ) ↔ ran 𝐹 ∈ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐿 )
2 1 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑋 ∈ 𝐿 )
3 simp1 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑌 ∈ 𝐴 )
4 simp3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐹 : 𝑌 ⟶ 𝑋 )
5 fmf ⊢ ( ( 𝑋 ∈ 𝐿 ∧ 𝑌 ∈ 𝐴 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) : ( fBas ‘ 𝑌 ) ⟶ ( Fil ‘ 𝑋 ) )
6 2 3 4 5 syl3anc ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) : ( fBas ‘ 𝑌 ) ⟶ ( Fil ‘ 𝑋 ) )
7 6 ffnd ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) Fn ( fBas ‘ 𝑌 ) )
8 fvelrnb ⊢ ( ( 𝑋 FilMap 𝐹 ) Fn ( fBas ‘ 𝑌 ) → ( 𝐿 ∈ ran ( 𝑋 FilMap 𝐹 ) ↔ ∃ 𝑏 ∈ ( fBas ‘ 𝑌 ) ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 ) )
9 7 8 syl ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐿 ∈ ran ( 𝑋 FilMap 𝐹 ) ↔ ∃ 𝑏 ∈ ( fBas ‘ 𝑌 ) ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 ) )
10 ffn ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 Fn 𝑌 )
11 dffn4 ⊢ ( 𝐹 Fn 𝑌 ↔ 𝐹 : 𝑌 –onto→ ran 𝐹 )
12 10 11 sylib ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 : 𝑌 –onto→ ran 𝐹 )
13 foima ⊢ ( 𝐹 : 𝑌 –onto→ ran 𝐹 → ( 𝐹 “ 𝑌 ) = ran 𝐹 )
14 12 13 syl ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝐹 “ 𝑌 ) = ran 𝐹 )
15 14 ad2antlr ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → ( 𝐹 “ 𝑌 ) = ran 𝐹 )
16 simpll ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → 𝑋 ∈ 𝐿 )
17 simpr ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → 𝑏 ∈ ( fBas ‘ 𝑌 ) )
18 simplr ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → 𝐹 : 𝑌 ⟶ 𝑋 )
19 fgcl ⊢ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝑏 ) ∈ ( Fil ‘ 𝑌 ) )
20 filtop ⊢ ( ( 𝑌 filGen 𝑏 ) ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ ( 𝑌 filGen 𝑏 ) )
21 19 20 syl ⊢ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ ( 𝑌 filGen 𝑏 ) )
22 21 adantl ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → 𝑌 ∈ ( 𝑌 filGen 𝑏 ) )
23 eqid ⊢ ( 𝑌 filGen 𝑏 ) = ( 𝑌 filGen 𝑏 )
24 23 imaelfm ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑌 ∈ ( 𝑌 filGen 𝑏 ) ) → ( 𝐹 “ 𝑌 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) )
25 16 17 18 22 24 syl31anc ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → ( 𝐹 “ 𝑌 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) )
26 15 25 eqeltrrd ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → ran 𝐹 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) )
27 eleq2 ⊢ ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 → ( ran 𝐹 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) ↔ ran 𝐹 ∈ 𝐿 ) )
28 26 27 syl5ibcom ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 → ran 𝐹 ∈ 𝐿 ) )
29 28 ex ⊢ ( ( 𝑋 ∈ 𝐿 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑏 ∈ ( fBas ‘ 𝑌 ) → ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 → ran 𝐹 ∈ 𝐿 ) ) )
30 1 29 sylan ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑏 ∈ ( fBas ‘ 𝑌 ) → ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 → ran 𝐹 ∈ 𝐿 ) ) )
31 30 3adant1 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑏 ∈ ( fBas ‘ 𝑌 ) → ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 → ran 𝐹 ∈ 𝐿 ) ) )
32 31 rexlimdv ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∃ 𝑏 ∈ ( fBas ‘ 𝑌 ) ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) = 𝐿 → ran 𝐹 ∈ 𝐿 ) )
33 9 32 sylbid ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐿 ∈ ran ( 𝑋 FilMap 𝐹 ) → ran 𝐹 ∈ 𝐿 ) )
34 simpl2 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
35 filelss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ∈ 𝐿 ) → 𝑡 ⊆ 𝑋 )
36 35 ex ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋 ) )
37 34 36 syl ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋 ) )
38 simpr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → 𝑡 ∈ 𝐿 )
39 eqidd ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑡 ) )
40 imaeq2 ⊢ ( 𝑥 = 𝑡 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑡 ) )
41 40 rspceeqv ⊢ ( ( 𝑡 ∈ 𝐿 ∧ ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑡 ) ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) )
42 38 39 41 syl2anc ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) )
43 simpl1 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝑌 ∈ 𝐴 )
44 cnvimass ⊢ ( ◡ 𝐹 “ 𝑡 ) ⊆ dom 𝐹
45 fdm ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → dom 𝐹 = 𝑌 )
46 44 45 sseqtrid ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( ◡ 𝐹 “ 𝑡 ) ⊆ 𝑌 )
47 46 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ◡ 𝐹 “ 𝑡 ) ⊆ 𝑌 )
48 47 adantr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ⊆ 𝑌 )
49 43 48 ssexd ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ V )
50 eqid ⊢ ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) )
51 50 elrnmpt ⊢ ( ( ◡ 𝐹 “ 𝑡 ) ∈ V → ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
52 49 51 syl ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
53 52 adantr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
54 42 53 mpbird ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
55 ssid ⊢ ( ◡ 𝐹 “ 𝑡 ) ⊆ ( ◡ 𝐹 “ 𝑡 )
56 ffun ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → Fun 𝐹 )
57 56 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → Fun 𝐹 )
58 57 ad2antrr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → Fun 𝐹 )
59 funimass3 ⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝑡 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ↔ ( ◡ 𝐹 “ 𝑡 ) ⊆ ( ◡ 𝐹 “ 𝑡 ) ) )
60 58 44 59 sylancl ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ↔ ( ◡ 𝐹 “ 𝑡 ) ⊆ ( ◡ 𝐹 “ 𝑡 ) ) )
61 55 60 mpbiri ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 )
62 imaeq2 ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑡 ) → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) )
63 62 sseq1d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑡 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) )
64 63 rspcev ⊢ ( ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) → ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 )
65 54 61 64 syl2anc ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑡 ∈ 𝐿 ) → ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 )
66 65 ex ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑡 ∈ 𝐿 → ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) )
67 37 66 jcad ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑡 ∈ 𝐿 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
68 34 adantr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ∧ 𝑡 ⊆ 𝑋 ) ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
69 50 elrnmpt ⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ) )
70 69 elv ⊢ ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) )
71 ssid ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ◡ 𝐹 “ 𝑥 )
72 57 ad3antrrr ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → Fun 𝐹 )
73 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
74 funimass3 ⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑥 ↔ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ◡ 𝐹 “ 𝑥 ) ) )
75 72 73 74 sylancl ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑥 ↔ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ◡ 𝐹 “ 𝑥 ) ) )
76 71 75 mpbiri ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑥 )
77 imassrn ⊢ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ran 𝐹
78 ssin ⊢ ( ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑥 ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ran 𝐹 ) ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( 𝑥 ∩ ran 𝐹 ) )
79 76 77 78 sylanblc ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( 𝑥 ∩ ran 𝐹 ) )
80 elin ⊢ ( 𝑧 ∈ ( 𝑥 ∩ ran 𝐹 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ ran 𝐹 ) )
81 fvelrnb ⊢ ( 𝐹 Fn 𝑌 → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = 𝑧 ) )
82 10 81 syl ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = 𝑧 ) )
83 82 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = 𝑧 ) )
84 83 ad3antrrr ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = 𝑧 ) )
85 72 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) → Fun 𝐹 )
86 85 73 jctir ⊢ ( ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) → ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹 ) )
87 57 ad2antrr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → Fun 𝐹 )
88 87 ad2antrr ⊢ ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → Fun 𝐹 )
89 45 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → dom 𝐹 = 𝑌 )
90 89 ad3antrrr ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → dom 𝐹 = 𝑌 )
91 90 eleq2d ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝑌 ) )
92 91 biimpar ⊢ ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ dom 𝐹 )
93 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
94 88 92 93 syl2anc ⊢ ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
95 94 biimpa ⊢ ( ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) )
96 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹 ) → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) )
97 86 95 96 sylc ⊢ ( ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) )
98 97 ex ⊢ ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) )
99 eleq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
100 eleq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ↔ 𝑧 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) )
101 99 100 imbi12d ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → ( ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ( 𝑧 ∈ 𝑥 → 𝑧 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
102 98 101 syl5ibcom ⊢ ( ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
103 102 rexlimdva ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = 𝑧 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
104 84 103 sylbid ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑧 ∈ ran 𝐹 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
105 104 impcomd ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ ran 𝐹 ) → 𝑧 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) )
106 80 105 biimtrid ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ ran 𝐹 ) → 𝑧 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) )
107 106 ssrdv ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑥 ∩ ran 𝐹 ) ⊆ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) )
108 79 107 eqssd ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝑥 ∩ ran 𝐹 ) )
109 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 )
110 109 3exp ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐿 → ( ran 𝐹 ∈ 𝐿 → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 ) ) )
111 110 com23 ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( ran 𝐹 ∈ 𝐿 → ( 𝑥 ∈ 𝐿 → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 ) ) )
112 111 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ran 𝐹 ∈ 𝐿 → ( 𝑥 ∈ 𝐿 → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 ) ) )
113 112 imp31 ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 )
114 113 adantr ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 )
115 108 114 eqeltrd ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝐿 )
116 115 exp32 ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝐿 ) ) )
117 imaeq2 ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) )
118 117 sseq1d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ) )
119 117 eleq1d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ∈ 𝐿 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝐿 ) )
120 119 imbi2d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ↔ ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝐿 ) ) )
121 118 120 imbi12d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ) ↔ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝐿 ) ) ) )
122 116 121 syl5ibrcom ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ) ) )
123 122 rexlimdva ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ) ) )
124 70 123 biimtrid ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ) ) )
125 124 imp44 ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ 𝑠 ) ∈ 𝐿 )
126 simprr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ⊆ 𝑋 )
127 simprlr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ 𝑠 ) ⊆ 𝑡 )
128 filss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝐹 “ 𝑠 ) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) → 𝑡 ∈ 𝐿 )
129 68 125 126 127 128 syl13anc ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ∈ 𝐿 )
130 129 exp44 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
131 130 rexlimdv ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
132 131 impcomd ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 ) )
133 67 132 impbid ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
134 2 adantr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝑋 ∈ 𝐿 )
135 rnelfmlem ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) )
136 simpl3 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝐹 : 𝑌 ⟶ 𝑋 )
137 elfm ⊢ ( ( 𝑋 ∈ 𝐿 ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
138 134 135 136 137 syl3anc ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
139 133 138 bitr4d ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
140 139 eqrdv ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) )
141 7 adantr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑋 FilMap 𝐹 ) Fn ( fBas ‘ 𝑌 ) )
142 fnfvelrn ⊢ ( ( ( 𝑋 FilMap 𝐹 ) Fn ( fBas ‘ 𝑌 ) ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ ran ( 𝑋 FilMap 𝐹 ) )
143 141 135 142 syl2anc ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ ran ( 𝑋 FilMap 𝐹 ) )
144 140 143 eqeltrd ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝐿 ∈ ran ( 𝑋 FilMap 𝐹 ) )
145 144 ex ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ran 𝐹 ∈ 𝐿 → 𝐿 ∈ ran ( 𝑋 FilMap 𝐹 ) ) )
146 33 145 impbid ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐿 ∈ ran ( 𝑋 FilMap 𝐹 ) ↔ ran 𝐹 ∈ 𝐿 ) )