Metamath Proof Explorer

Theorem fmfnfmlem4

Description: Lemma for fmfnfm . (Contributed by Jeff Hankins, 19-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 fmfnfmlem4 ( 𝜑 → ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
2 fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
3 fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
4 fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
5 filelss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ∈ 𝐿 ) → 𝑡 ⊆ 𝑋 )
6 5 ex ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋 ) )
7 2 6 syl ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋 ) )
8 mptexg ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V )
9 rnexg ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V )
10 8 9 syl ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V )
11 2 10 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V )
12 unexg ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V )
13 1 11 12 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V )
14 ssfii ⊢ ( ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
15 14 unssbd ⊢ ( ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
16 13 15 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
18 eqid ⊢ ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑡 )
19 imaeq2 ⊢ ( 𝑥 = 𝑡 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑡 ) )
20 19 rspceeqv ⊢ ( ( 𝑡 ∈ 𝐿 ∧ ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑡 ) ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) )
21 18 20 mpan2 ⊢ ( 𝑡 ∈ 𝐿 → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) )
23 elfvdm ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ dom fBas )
24 1 23 syl ⊢ ( 𝜑 → 𝑌 ∈ dom fBas )
25 cnvimass ⊢ ( ◡ 𝐹 “ 𝑡 ) ⊆ dom 𝐹
26 25 3 fssdm ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑡 ) ⊆ 𝑌 )
27 24 26 ssexd ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑡 ) ∈ V )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ V )
29 eqid ⊢ ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) )
30 29 elrnmpt ⊢ ( ( ◡ 𝐹 “ 𝑡 ) ∈ V → ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
31 28 30 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
32 22 31 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
33 17 32 sseldd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
34 ffun ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → Fun 𝐹 )
35 ssid ⊢ ( ◡ 𝐹 “ 𝑡 ) ⊆ ( ◡ 𝐹 “ 𝑡 )
36 funimass2 ⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝑡 ) ⊆ ( ◡ 𝐹 “ 𝑡 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 )
37 34 35 36 sylancl ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 )
38 3 37 syl ⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 )
40 imaeq2 ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑡 ) → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) )
41 40 sseq1d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑡 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) )
42 41 rspcev ⊢ ( ( ( ◡ 𝐹 “ 𝑡 ) ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) → ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 )
43 33 39 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 )
44 43 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 → ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) )
45 7 44 jcad ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )
46 elfiun ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) → ( 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ( 𝑠 ∈ ( fi ‘ 𝐵 ) ∨ 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∨ ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) ) ) )
47 1 11 46 syl2anc ⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ( 𝑠 ∈ ( fi ‘ 𝐵 ) ∨ 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∨ ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) ) ) )
48 1 2 3 4 fmfnfmlem1 ⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ 𝐵 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
49 1 2 3 4 fmfnfmlem3 ⊢ ( 𝜑 → ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
50 49 eleq2d ⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) )
51 29 elrnmpt ⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ) )
52 51 elv ⊢ ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) )
53 1 2 3 4 fmfnfmlem2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
54 52 53 syl5bi ⊢ ( 𝜑 → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
55 50 54 sylbid ⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
56 49 eleq2d ⊢ ( 𝜑 → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) )
57 29 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) ) )
58 57 elv ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) )
59 56 58 bitrdi ⊢ ( 𝜑 → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) ) )
61 fbssfi ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 )
62 1 61 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 )
63 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
64 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
65 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
66 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐿 )
67 2 66 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
68 67 1 3 3jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) )
70 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) )
71 1 70 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) )
72 71 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ∈ ( 𝑌 filGen 𝐵 ) )
73 eqid ⊢ ( 𝑌 filGen 𝐵 ) = ( 𝑌 filGen 𝐵 )
74 73 imaelfm ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑠 ∈ ( 𝑌 filGen 𝐵 ) ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
75 69 72 74 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
76 65 75 sseldd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝐹 “ 𝑠 ) ∈ 𝐿 )
77 76 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → ( 𝐹 “ 𝑠 ) ∈ 𝐿 )
78 64 77 jca ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) )
79 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 )
80 79 3expa ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 )
81 78 80 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 )
82 81 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 )
83 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ⊆ 𝑋 )
84 elin ⊢ ( 𝑤 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ↔ ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) ∧ 𝑤 ∈ 𝑥 ) )
85 3 34 syl ⊢ ( 𝜑 → Fun 𝐹 )
86 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑤 ∈ ( 𝐹 “ 𝑠 ) ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 )
87 86 ex ⊢ ( Fun 𝐹 → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 ) )
88 85 87 syl ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 ) )
89 88 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 ) )
90 85 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → Fun 𝐹 )
91 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → 𝑠 ⊆ 𝑧 )
92 simprl ⊢ ( ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) → 𝑦 ∈ 𝑠 )
93 ssel2 ⊢ ( ( 𝑠 ⊆ 𝑧 ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ 𝑧 )
94 91 92 93 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → 𝑦 ∈ 𝑧 )
95 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → Fun 𝐹 )
96 fbelss ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ 𝑌 )
97 1 96 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ 𝑌 )
98 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑌 )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → dom 𝐹 = 𝑌 )
100 97 99 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ dom 𝐹 )
101 100 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → 𝑠 ⊆ dom 𝐹 )
102 101 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ dom 𝐹 )
103 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
104 95 102 103 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
105 104 biimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
106 105 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) )
107 106 ad2ant2rl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) )
108 94 107 elind ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → 𝑦 ∈ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) )
109 inss2 ⊢ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 )
110 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
111 109 110 sstri ⊢ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ dom 𝐹
112 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ dom 𝐹 ) → ( 𝑦 ∈ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
113 111 112 mpan2 ⊢ ( Fun 𝐹 → ( 𝑦 ∈ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
114 90 108 113 sylc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) )
115 114 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) )
116 115 expr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
117 eleq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) )
118 eleq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
119 117 118 imbi12d ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
120 116 119 syl5ibcom ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
121 120 rexlimdva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
122 89 121 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) )
123 122 impd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) ∧ 𝑤 ∈ 𝑥 ) → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
124 84 123 syl5bi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( 𝑤 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
125 124 adantrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑤 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
126 125 ssrdv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ⊆ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) )
127 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 )
128 126 127 sstrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ⊆ 𝑡 )
129 filss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ⊆ 𝑡 ) ) → 𝑡 ∈ 𝐿 )
130 63 82 83 128 129 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ∈ 𝐿 )
131 130 exp32 ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
132 ineq2 ⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝑧 ∩ 𝑤 ) = ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) )
133 132 imaeq2d ⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) = ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) )
134 133 sseq1d ⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 ↔ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ) )
135 134 imbi1d ⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ↔ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
136 131 135 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
137 136 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
138 137 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) )
139 138 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 ) → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
140 62 139 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
141 60 140 sylbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
142 141 impr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
143 imaeq2 ⊢ ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) )
144 143 sseq1d ⊢ ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ↔ ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 ) )
145 144 imbi1d ⊢ ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ↔ ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
146 142 145 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
147 146 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
148 48 55 147 3jaod ⊢ ( 𝜑 → ( ( 𝑠 ∈ ( fi ‘ 𝐵 ) ∨ 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∨ ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
149 47 148 sylbid ⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
150 149 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
151 150 impcomd ⊢ ( 𝜑 → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 ) )
152 45 151 impbid ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) )