MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmfnfmlem4 Structured version   Visualization version   GIF version

Theorem fmfnfmlem4 23324
Description: Lemma for fmfnfm 23325. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Hypotheses
Ref Expression
fmfnfm.b (πœ‘ β†’ 𝐡 ∈ (fBasβ€˜π‘Œ))
fmfnfm.l (πœ‘ β†’ 𝐿 ∈ (Filβ€˜π‘‹))
fmfnfm.f (πœ‘ β†’ 𝐹:π‘ŒβŸΆπ‘‹)
fmfnfm.fm (πœ‘ β†’ ((𝑋 FilMap 𝐹)β€˜π΅) βŠ† 𝐿)
Assertion
Ref Expression
fmfnfmlem4 (πœ‘ β†’ (𝑑 ∈ 𝐿 ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)))
Distinct variable groups:   𝑑,𝑠,π‘₯,𝐡   𝐹,𝑠,𝑑,π‘₯   𝐿,𝑠,𝑑,π‘₯   πœ‘,𝑠,𝑑,π‘₯   𝑋,𝑠,𝑑,π‘₯   π‘Œ,𝑠,𝑑,π‘₯

Proof of Theorem fmfnfmlem4
Dummy variables 𝑀 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmfnfm.l . . . 4 (πœ‘ β†’ 𝐿 ∈ (Filβ€˜π‘‹))
2 filelss 23219 . . . . 5 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝑑 ∈ 𝐿) β†’ 𝑑 βŠ† 𝑋)
32ex 414 . . . 4 (𝐿 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ 𝐿 β†’ 𝑑 βŠ† 𝑋))
41, 3syl 17 . . 3 (πœ‘ β†’ (𝑑 ∈ 𝐿 β†’ 𝑑 βŠ† 𝑋))
5 fmfnfm.b . . . . . . . . 9 (πœ‘ β†’ 𝐡 ∈ (fBasβ€˜π‘Œ))
6 mptexg 7176 . . . . . . . . . . 11 (𝐿 ∈ (Filβ€˜π‘‹) β†’ (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
7 rnexg 7846 . . . . . . . . . . 11 ((π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
86, 7syl 17 . . . . . . . . . 10 (𝐿 ∈ (Filβ€˜π‘‹) β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
91, 8syl 17 . . . . . . . . 9 (πœ‘ β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
10 unexg 7688 . . . . . . . . 9 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V) β†’ (𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V)
115, 9, 10syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V)
12 ssfii 9362 . . . . . . . . 9 ((𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V β†’ (𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
1312unssbd 4153 . . . . . . . 8 ((𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
1411, 13syl 17 . . . . . . 7 (πœ‘ β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
1514adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
16 eqid 2737 . . . . . . . . 9 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ 𝑑)
17 imaeq2 6014 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (◑𝐹 β€œ π‘₯) = (◑𝐹 β€œ 𝑑))
1817rspceeqv 3600 . . . . . . . . 9 ((𝑑 ∈ 𝐿 ∧ (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ 𝑑)) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯))
1916, 18mpan2 690 . . . . . . . 8 (𝑑 ∈ 𝐿 β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯))
2019adantl 483 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯))
21 elfvdm 6884 . . . . . . . . . . 11 (𝐡 ∈ (fBasβ€˜π‘Œ) β†’ π‘Œ ∈ dom fBas)
225, 21syl 17 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ dom fBas)
23 cnvimass 6038 . . . . . . . . . . 11 (◑𝐹 β€œ 𝑑) βŠ† dom 𝐹
24 fmfnfm.f . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:π‘ŒβŸΆπ‘‹)
2523, 24fssdm 6693 . . . . . . . . . 10 (πœ‘ β†’ (◑𝐹 β€œ 𝑑) βŠ† π‘Œ)
2622, 25ssexd 5286 . . . . . . . . 9 (πœ‘ β†’ (◑𝐹 β€œ 𝑑) ∈ V)
2726adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (◑𝐹 β€œ 𝑑) ∈ V)
28 eqid 2737 . . . . . . . . 9 (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) = (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))
2928elrnmpt 5916 . . . . . . . 8 ((◑𝐹 β€œ 𝑑) ∈ V β†’ ((◑𝐹 β€œ 𝑑) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯)))
3027, 29syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ ((◑𝐹 β€œ 𝑑) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯)))
3120, 30mpbird 257 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (◑𝐹 β€œ 𝑑) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
3215, 31sseldd 3950 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (◑𝐹 β€œ 𝑑) ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
33 ffun 6676 . . . . . . . 8 (𝐹:π‘ŒβŸΆπ‘‹ β†’ Fun 𝐹)
34 ssid 3971 . . . . . . . 8 (◑𝐹 β€œ 𝑑) βŠ† (◑𝐹 β€œ 𝑑)
35 funimass2 6589 . . . . . . . 8 ((Fun 𝐹 ∧ (◑𝐹 β€œ 𝑑) βŠ† (◑𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
3633, 34, 35sylancl 587 . . . . . . 7 (𝐹:π‘ŒβŸΆπ‘‹ β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
3724, 36syl 17 . . . . . 6 (πœ‘ β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
3837adantr 482 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
39 imaeq2 6014 . . . . . . 7 (𝑠 = (◑𝐹 β€œ 𝑑) β†’ (𝐹 β€œ 𝑠) = (𝐹 β€œ (◑𝐹 β€œ 𝑑)))
4039sseq1d 3980 . . . . . 6 (𝑠 = (◑𝐹 β€œ 𝑑) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 ↔ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑))
4140rspcev 3584 . . . . 5 (((◑𝐹 β€œ 𝑑) ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) ∧ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑) β†’ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)
4232, 38, 41syl2anc 585 . . . 4 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)
4342ex 414 . . 3 (πœ‘ β†’ (𝑑 ∈ 𝐿 β†’ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑))
444, 43jcad 514 . 2 (πœ‘ β†’ (𝑑 ∈ 𝐿 β†’ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)))
45 elfiun 9373 . . . . . 6 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V) β†’ (𝑠 ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) ↔ (𝑠 ∈ (fiβ€˜π΅) ∨ 𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∨ βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀))))
465, 9, 45syl2anc 585 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) ↔ (𝑠 ∈ (fiβ€˜π΅) ∨ 𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∨ βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀))))
47 fmfnfm.fm . . . . . . 7 (πœ‘ β†’ ((𝑋 FilMap 𝐹)β€˜π΅) βŠ† 𝐿)
485, 1, 24, 47fmfnfmlem1 23321 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜π΅) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
495, 1, 24, 47fmfnfmlem3 23323 . . . . . . . 8 (πœ‘ β†’ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) = ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
5049eleq2d 2824 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ 𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))
5128elrnmpt 5916 . . . . . . . . 9 (𝑠 ∈ V β†’ (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯)))
5251elv 3454 . . . . . . . 8 (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯))
535, 1, 24, 47fmfnfmlem2 23322 . . . . . . . 8 (πœ‘ β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
5452, 53biimtrid 241 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
5550, 54sylbid 239 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
5649eleq2d 2824 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ 𝑀 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))
5728elrnmpt 5916 . . . . . . . . . . . . 13 (𝑀 ∈ V β†’ (𝑀 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯)))
5857elv 3454 . . . . . . . . . . . 12 (𝑀 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯))
5956, 58bitrdi 287 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯)))
6059adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯)))
61 fbssfi 23204 . . . . . . . . . . . 12 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧)
625, 61sylan 581 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧)
631ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ 𝐿 ∈ (Filβ€˜π‘‹))
641adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ 𝐿 ∈ (Filβ€˜π‘‹))
6547adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ ((𝑋 FilMap 𝐹)β€˜π΅) βŠ† 𝐿)
66 filtop 23222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐿 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐿)
671, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑋 ∈ 𝐿)
6867, 5, 243jca 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑋 ∈ 𝐿 ∧ 𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝐹:π‘ŒβŸΆπ‘‹))
6968adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ (𝑋 ∈ 𝐿 ∧ 𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝐹:π‘ŒβŸΆπ‘‹))
70 ssfg 23239 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐡 ∈ (fBasβ€˜π‘Œ) β†’ 𝐡 βŠ† (π‘ŒfilGen𝐡))
715, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐡 βŠ† (π‘ŒfilGen𝐡))
7271sselda 3949 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 ∈ (π‘ŒfilGen𝐡))
73 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘ŒfilGen𝐡) = (π‘ŒfilGen𝐡)
7473imaelfm 23318 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋 ∈ 𝐿 ∧ 𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ 𝑠 ∈ (π‘ŒfilGen𝐡)) β†’ (𝐹 β€œ 𝑠) ∈ ((𝑋 FilMap 𝐹)β€˜π΅))
7569, 72, 74syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ (𝐹 β€œ 𝑠) ∈ ((𝑋 FilMap 𝐹)β€˜π΅))
7665, 75sseldd 3950 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ (𝐹 β€œ 𝑠) ∈ 𝐿)
7776adantrr 716 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ (𝐹 β€œ 𝑠) ∈ 𝐿)
7864, 77jca 513 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ (𝐿 ∈ (Filβ€˜π‘‹) ∧ (𝐹 β€œ 𝑠) ∈ 𝐿))
79 filin 23221 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ (𝐹 β€œ 𝑠) ∈ 𝐿 ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
80793expa 1119 . . . . . . . . . . . . . . . . . . 19 (((𝐿 ∈ (Filβ€˜π‘‹) ∧ (𝐹 β€œ 𝑠) ∈ 𝐿) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
8178, 80sylan 581 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
8281adantr 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
83 simprr 772 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ 𝑑 βŠ† 𝑋)
84 elin 3931 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ((𝐹 β€œ 𝑠) ∩ π‘₯) ↔ (𝑀 ∈ (𝐹 β€œ 𝑠) ∧ 𝑀 ∈ π‘₯))
8524, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ Fun 𝐹)
86 fvelima 6913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹 ∧ 𝑀 ∈ (𝐹 β€œ 𝑠)) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀)
8786ex 414 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun 𝐹 β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀))
8885, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀))
8988ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀))
9085ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ Fun 𝐹)
91 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ 𝑠 βŠ† 𝑧)
92 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯)) β†’ 𝑦 ∈ 𝑠)
93 ssel2 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 βŠ† 𝑧 ∧ 𝑦 ∈ 𝑠) β†’ 𝑦 ∈ 𝑧)
9491, 92, 93syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ 𝑦 ∈ 𝑧)
9585ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ Fun 𝐹)
96 fbelss 23200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 βŠ† π‘Œ)
975, 96sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 βŠ† π‘Œ)
9824fdmd 6684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (πœ‘ β†’ dom 𝐹 = π‘Œ)
9998adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ dom 𝐹 = π‘Œ)
10097, 99sseqtrrd 3990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 βŠ† dom 𝐹)
101100adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ 𝑠 βŠ† dom 𝐹)
102101sselda 3949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ 𝑦 ∈ dom 𝐹)
103 fvimacnv 7008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ ↔ 𝑦 ∈ (◑𝐹 β€œ π‘₯)))
10495, 102, 103syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ ↔ 𝑦 ∈ (◑𝐹 β€œ π‘₯)))
105104biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ β†’ 𝑦 ∈ (◑𝐹 β€œ π‘₯)))
106105impr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯)) β†’ 𝑦 ∈ (◑𝐹 β€œ π‘₯))
107106ad2ant2rl 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ 𝑦 ∈ (◑𝐹 β€œ π‘₯))
10894, 107elind 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ 𝑦 ∈ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))
109 inss2 4194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∩ (◑𝐹 β€œ π‘₯)) βŠ† (◑𝐹 β€œ π‘₯)
110 cnvimass 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (◑𝐹 β€œ π‘₯) βŠ† dom 𝐹
111109, 110sstri 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∩ (◑𝐹 β€œ π‘₯)) βŠ† dom 𝐹
112 funfvima2 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun 𝐹 ∧ (𝑧 ∩ (◑𝐹 β€œ π‘₯)) βŠ† dom 𝐹) β†’ (𝑦 ∈ (𝑧 ∩ (◑𝐹 β€œ π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
113111, 112mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝐹 β†’ (𝑦 ∈ (𝑧 ∩ (◑𝐹 β€œ π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
11490, 108, 113sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
115114anassrs 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
116115expr 458 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
117 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πΉβ€˜π‘¦) = 𝑀 β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ ↔ 𝑀 ∈ π‘₯))
118 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πΉβ€˜π‘¦) = 𝑀 β†’ ((πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) ↔ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
119117, 118imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πΉβ€˜π‘¦) = 𝑀 β†’ (((πΉβ€˜π‘¦) ∈ π‘₯ β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))) ↔ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
120116, 119syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) = 𝑀 β†’ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
121120rexlimdva 3153 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀 β†’ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
12289, 121syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
123122impd 412 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ ((𝑀 ∈ (𝐹 β€œ 𝑠) ∧ 𝑀 ∈ π‘₯) β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
12484, 123biimtrid 241 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (𝑀 ∈ ((𝐹 β€œ 𝑠) ∩ π‘₯) β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
125124adantrl 715 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ (𝑀 ∈ ((𝐹 β€œ 𝑠) ∩ π‘₯) β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
126125ssrdv 3955 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) βŠ† (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
127 simprl 770 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑)
128126, 127sstrd 3959 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) βŠ† 𝑑)
129 filss 23220 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ (((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿 ∧ 𝑑 βŠ† 𝑋 ∧ ((𝐹 β€œ 𝑠) ∩ π‘₯) βŠ† 𝑑)) β†’ 𝑑 ∈ 𝐿)
13063, 82, 83, 128, 129syl13anc 1373 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ 𝑑 ∈ 𝐿)
131130exp32 422 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))
132 ineq2 4171 . . . . . . . . . . . . . . . . . 18 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ (𝑧 ∩ 𝑀) = (𝑧 ∩ (◑𝐹 β€œ π‘₯)))
133132imaeq2d 6018 . . . . . . . . . . . . . . . . 17 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ (𝐹 β€œ (𝑧 ∩ 𝑀)) = (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
134133sseq1d 3980 . . . . . . . . . . . . . . . 16 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 ↔ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑))
135134imbi1d 342 . . . . . . . . . . . . . . 15 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ (((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)) ↔ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
136131, 135syl5ibrcom 247 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ (𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
137136rexlimdva 3153 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
138137rexlimdvaa 3154 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧 β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))))
139138imp 408 . . . . . . . . . . 11 ((πœ‘ ∧ βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧) β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14062, 139syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14160, 140sylbid 239 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
142141impr 456 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ 𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))
143 imaeq2 6014 . . . . . . . . . 10 (𝑠 = (𝑧 ∩ 𝑀) β†’ (𝐹 β€œ 𝑠) = (𝐹 β€œ (𝑧 ∩ 𝑀)))
144143sseq1d 3980 . . . . . . . . 9 (𝑠 = (𝑧 ∩ 𝑀) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 ↔ (𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑))
145144imbi1d 342 . . . . . . . 8 (𝑠 = (𝑧 ∩ 𝑀) β†’ (((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)) ↔ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
146142, 145syl5ibrcom 247 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ 𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))) β†’ (𝑠 = (𝑧 ∩ 𝑀) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
147146rexlimdvva 3206 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14848, 55, 1473jaod 1429 . . . . 5 (πœ‘ β†’ ((𝑠 ∈ (fiβ€˜π΅) ∨ 𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∨ βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀)) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14946, 148sylbid 239 . . . 4 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
150149rexlimdv 3151 . . 3 (πœ‘ β†’ (βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))
151150impcomd 413 . 2 (πœ‘ β†’ ((𝑑 βŠ† 𝑋 ∧ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑) β†’ 𝑑 ∈ 𝐿))
15244, 151impbid 211 1 (πœ‘ β†’ (𝑑 ∈ 𝐿 ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ w3o 1087   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆƒwrex 3074  Vcvv 3448   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915   ↦ cmpt 5193  β—‘ccnv 5637  dom cdm 5638  ran crn 5639   β€œ cima 5641  Fun wfun 6495  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  ficfi 9353  fBascfbas 20800  filGencfg 20801  Filcfil 23212   FilMap cfm 23300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1o 8417  df-er 8655  df-en 8891  df-fin 8894  df-fi 9354  df-fbas 20809  df-fg 20810  df-fil 23213  df-fm 23305
This theorem is referenced by:  fmfnfm  23325
  Copyright terms: Public domain W3C validator