Metamath Proof Explorer

Theorem rnelfmlem

Description: Lemma for rnelfm . (Contributed by Jeff Hankins, 14-Nov-2009)

Ref Expression
Assertion rnelfmlem ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝑌 ∈ 𝐴 )
2 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
3 simpl3 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝐹 : 𝑌 ⟶ 𝑋 )
4 2 3 fssdm ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝑌 )
5 1 4 sselpwd ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝒫 𝑌 )
6 5 adantr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝒫 𝑌 )
7 6 fmpttd ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) : 𝐿 ⟶ 𝒫 𝑌 )
8 7 frnd ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝒫 𝑌 )
9 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐿 )
10 9 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑋 ∈ 𝐿 )
11 10 adantr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝑋 ∈ 𝐿 )
12 fimacnv ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( ◡ 𝐹 “ 𝑋 ) = 𝑌 )
13 12 eqcomd ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝑌 = ( ◡ 𝐹 “ 𝑋 ) )
14 13 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑌 = ( ◡ 𝐹 “ 𝑋 ) )
15 14 adantr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝑌 = ( ◡ 𝐹 “ 𝑋 ) )
16 imaeq2 ⊢ ( 𝑥 = 𝑋 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑋 ) )
17 16 rspceeqv ⊢ ( ( 𝑋 ∈ 𝐿 ∧ 𝑌 = ( ◡ 𝐹 “ 𝑋 ) ) → ∃ 𝑥 ∈ 𝐿 𝑌 = ( ◡ 𝐹 “ 𝑥 ) )
18 11 15 17 syl2anc ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ∃ 𝑥 ∈ 𝐿 𝑌 = ( ◡ 𝐹 “ 𝑥 ) )
19 eqid ⊢ ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) )
20 19 elrnmpt ⊢ ( 𝑌 ∈ 𝐴 → ( 𝑌 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑌 = ( ◡ 𝐹 “ 𝑥 ) ) )
21 20 3ad2ant1 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑌 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑌 = ( ◡ 𝐹 “ 𝑥 ) ) )
22 21 adantr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑌 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑌 = ( ◡ 𝐹 “ 𝑥 ) ) )
23 18 22 mpbird ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → 𝑌 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
24 23 ne0d ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ )
25 0nelfil ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐿 )
26 25 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ¬ ∅ ∈ 𝐿 )
27 26 adantr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ¬ ∅ ∈ 𝐿 )
28 0ex ⊢ ∅ ∈ V
29 19 elrnmpt ⊢ ( ∅ ∈ V → ( ∅ ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ∅ = ( ◡ 𝐹 “ 𝑥 ) ) )
30 28 29 ax-mp ⊢ ( ∅ ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ∅ = ( ◡ 𝐹 “ 𝑥 ) )
31 ffn ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 Fn 𝑌 )
32 fvelrnb ⊢ ( 𝐹 Fn 𝑌 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
33 31 32 syl ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
34 33 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
35 34 ad2antrr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
36 eleq1 ⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
37 36 biimparc ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 )
38 37 ad2ant2l ⊢ ( ( ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 )
39 38 adantll ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑧 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 )
40 ffun ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → Fun 𝐹 )
41 40 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → Fun 𝐹 )
42 41 ad3antrrr ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑧 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → Fun 𝐹 )
43 fdm ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → dom 𝐹 = 𝑌 )
44 43 eleq2d ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝑌 ) )
45 44 biimpar ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑧 ∈ 𝑌 ) → 𝑧 ∈ dom 𝐹 )
46 45 3ad2antl3 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑧 ∈ 𝑌 ) → 𝑧 ∈ dom 𝐹 )
47 46 adantlr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑧 ∈ 𝑌 ) → 𝑧 ∈ dom 𝐹 )
48 47 ad2ant2r ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑧 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → 𝑧 ∈ dom 𝐹 )
49 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 ↔ 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
50 42 48 49 syl2anc ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑧 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 ↔ 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
51 39 50 mpbid ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑧 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) )
52 n0i ⊢ ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) → ¬ ( ◡ 𝐹 “ 𝑥 ) = ∅ )
53 eqcom ⊢ ( ( ◡ 𝐹 “ 𝑥 ) = ∅ ↔ ∅ = ( ◡ 𝐹 “ 𝑥 ) )
54 52 53 sylnib ⊢ ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) → ¬ ∅ = ( ◡ 𝐹 “ 𝑥 ) )
55 51 54 syl ⊢ ( ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑧 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → ¬ ∅ = ( ◡ 𝐹 “ 𝑥 ) )
56 55 rexlimdvaa ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) → ( ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 → ¬ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) )
57 35 56 sylbid ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑦 ∈ ran 𝐹 → ¬ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) )
58 57 con2d ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥 ) ) → ( ∅ = ( ◡ 𝐹 “ 𝑥 ) → ¬ 𝑦 ∈ ran 𝐹 ) )
59 58 expr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑦 ∈ 𝑥 → ( ∅ = ( ◡ 𝐹 “ 𝑥 ) → ¬ 𝑦 ∈ ran 𝐹 ) ) )
60 59 com23 ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ∅ = ( ◡ 𝐹 “ 𝑥 ) → ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹 ) ) )
61 60 impr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹 ) )
62 61 alrimiv ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹 ) )
63 imnan ⊢ ( ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹 ) ↔ ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹 ) )
64 elin ⊢ ( 𝑦 ∈ ( 𝑥 ∩ ran 𝐹 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹 ) )
65 63 64 xchbinxr ⊢ ( ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹 ) ↔ ¬ 𝑦 ∈ ( 𝑥 ∩ ran 𝐹 ) )
66 65 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹 ) ↔ ∀ 𝑦 ¬ 𝑦 ∈ ( 𝑥 ∩ ran 𝐹 ) )
67 eq0 ⊢ ( ( 𝑥 ∩ ran 𝐹 ) = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ ( 𝑥 ∩ ran 𝐹 ) )
68 eqcom ⊢ ( ( 𝑥 ∩ ran 𝐹 ) = ∅ ↔ ∅ = ( 𝑥 ∩ ran 𝐹 ) )
69 66 67 68 3bitr2i ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹 ) ↔ ∅ = ( 𝑥 ∩ ran 𝐹 ) )
70 62 69 sylib ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → ∅ = ( 𝑥 ∩ ran 𝐹 ) )
71 simpll2 ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
72 simprl ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → 𝑥 ∈ 𝐿 )
73 simplr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → ran 𝐹 ∈ 𝐿 )
74 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 )
75 71 72 73 74 syl3anc ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 )
76 70 75 eqeltrd ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝐿 ∧ ∅ = ( ◡ 𝐹 “ 𝑥 ) ) ) → ∅ ∈ 𝐿 )
77 76 rexlimdvaa ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ∃ 𝑥 ∈ 𝐿 ∅ = ( ◡ 𝐹 “ 𝑥 ) → ∅ ∈ 𝐿 ) )
78 30 77 syl5bi ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ∅ ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) → ∅ ∈ 𝐿 ) )
79 27 78 mtod ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ¬ ∅ ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
80 df-nel ⊢ ( ∅ ∉ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ¬ ∅ ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
81 79 80 sylibr ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ∅ ∉ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
82 19 elrnmpt ⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑟 = ( ◡ 𝐹 “ 𝑥 ) ) )
83 82 elv ⊢ ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑟 = ( ◡ 𝐹 “ 𝑥 ) )
84 imaeq2 ⊢ ( 𝑥 = 𝑢 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑢 ) )
85 84 eqeq2d ⊢ ( 𝑥 = 𝑢 → ( 𝑟 = ( ◡ 𝐹 “ 𝑥 ) ↔ 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ) )
86 85 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐿 𝑟 = ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑢 ∈ 𝐿 𝑟 = ( ◡ 𝐹 “ 𝑢 ) )
87 83 86 bitri ⊢ ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑢 ∈ 𝐿 𝑟 = ( ◡ 𝐹 “ 𝑢 ) )
88 19 elrnmpt ⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ) )
89 88 elv ⊢ ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) )
90 imaeq2 ⊢ ( 𝑥 = 𝑣 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑣 ) )
91 90 eqeq2d ⊢ ( 𝑥 = 𝑣 → ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ↔ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) )
92 91 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑣 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑣 ) )
93 89 92 bitri ⊢ ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑣 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑣 ) )
94 87 93 anbi12i ⊢ ( ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ( ∃ 𝑢 ∈ 𝐿 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ ∃ 𝑣 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) )
95 reeanv ⊢ ( ∃ 𝑢 ∈ 𝐿 ∃ 𝑣 ∈ 𝐿 ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ↔ ( ∃ 𝑢 ∈ 𝐿 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ ∃ 𝑣 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) )
96 94 95 bitr4i ⊢ ( ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ∃ 𝑢 ∈ 𝐿 ∃ 𝑣 ∈ 𝐿 ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) )
97 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝐿 )
98 97 3expb ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝐿 )
99 98 adantlr ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝐿 )
100 eqidd ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) )
101 imaeq2 ⊢ ( 𝑥 = ( 𝑢 ∩ 𝑣 ) → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) )
102 101 rspceeqv ⊢ ( ( ( 𝑢 ∩ 𝑣 ) ∈ 𝐿 ∧ ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
103 99 100 102 syl2anc ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
104 103 3adantl1 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
105 104 ad2ant2r ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
106 simpll1 ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → 𝑌 ∈ 𝐴 )
107 cnvimass ⊢ ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ dom 𝐹
108 107 43 sseqtrid ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ 𝑌 )
109 108 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ 𝑌 )
110 109 ad2antrr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ 𝑌 )
111 106 110 ssexd ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ∈ V )
112 19 elrnmpt ⊢ ( ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ∈ V → ( ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ 𝑥 ) ) )
113 111 112 syl ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ◡ 𝐹 “ 𝑥 ) ) )
114 105 113 mpbird ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
115 simprrl ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → 𝑟 = ( ◡ 𝐹 “ 𝑢 ) )
116 simprrr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → 𝑠 = ( ◡ 𝐹 “ 𝑣 ) )
117 115 116 ineq12d ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( 𝑟 ∩ 𝑠 ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
118 funcnvcnv ⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
119 imain ⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
120 40 118 119 3syl ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
121 120 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
122 121 ad2antrr ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝑣 ) ) )
123 117 122 eqtr4d ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( 𝑟 ∩ 𝑠 ) = ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) )
124 eqimss2 ⊢ ( ( 𝑟 ∩ 𝑠 ) = ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝑟 ∩ 𝑠 ) )
125 123 124 syl ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝑟 ∩ 𝑠 ) )
126 sseq1 ⊢ ( 𝑡 = ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) → ( 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ↔ ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝑟 ∩ 𝑠 ) ) )
127 126 rspcev ⊢ ( ( ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝑟 ∩ 𝑠 ) ) → ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) )
128 114 125 127 syl2anc ⊢ ( ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) ∧ ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) ∧ ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) ) ) → ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) )
129 128 exp32 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ( 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿 ) → ( ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) → ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) )
130 129 rexlimdvv ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ∃ 𝑢 ∈ 𝐿 ∃ 𝑣 ∈ 𝐿 ( 𝑟 = ( ◡ 𝐹 “ 𝑢 ) ∧ 𝑠 = ( ◡ 𝐹 “ 𝑣 ) ) → ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
131 96 130 syl5bi ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) → ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
132 131 ralrimivv ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ∀ 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∀ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) )
133 24 81 132 3jca ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ∧ ∅ ∉ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ∀ 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∀ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
134 isfbas2 ⊢ ( 𝑌 ∈ 𝐴 → ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) ↔ ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝒫 𝑌 ∧ ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ∧ ∅ ∉ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ∀ 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∀ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) )
135 1 134 syl ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) ↔ ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝒫 𝑌 ∧ ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ≠ ∅ ∧ ∅ ∉ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ ∀ 𝑟 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∀ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∃ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) )
136 8 133 135 mpbir2and ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ran 𝐹 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( fBas ‘ 𝑌 ) )