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

Theorem fmfnfmlem4 23468
Description: Lemma for fmfnfm 23469. (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 23363 . . . . 5 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝑑 ∈ 𝐿) β†’ 𝑑 βŠ† 𝑋)
32ex 413 . . . 4 (𝐿 ∈ (Filβ€˜π‘‹) β†’ (𝑑 ∈ 𝐿 β†’ 𝑑 βŠ† 𝑋))
41, 3syl 17 . . 3 (πœ‘ β†’ (𝑑 ∈ 𝐿 β†’ 𝑑 βŠ† 𝑋))
5 fmfnfm.b . . . . . . . . 9 (πœ‘ β†’ 𝐡 ∈ (fBasβ€˜π‘Œ))
6 mptexg 7225 . . . . . . . . . . 11 (𝐿 ∈ (Filβ€˜π‘‹) β†’ (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
7 rnexg 7897 . . . . . . . . . . 11 ((π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
86, 7syl 17 . . . . . . . . . 10 (𝐿 ∈ (Filβ€˜π‘‹) β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
91, 8syl 17 . . . . . . . . 9 (πœ‘ β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V)
10 unexg 7738 . . . . . . . . 9 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V) β†’ (𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V)
115, 9, 10syl2anc 584 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V)
12 ssfii 9416 . . . . . . . . 9 ((𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V β†’ (𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
1312unssbd 4188 . . . . . . . 8 ((𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∈ V β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
1411, 13syl 17 . . . . . . 7 (πœ‘ β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
1514adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) βŠ† (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
16 eqid 2732 . . . . . . . . 9 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ 𝑑)
17 imaeq2 6055 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (◑𝐹 β€œ π‘₯) = (◑𝐹 β€œ 𝑑))
1817rspceeqv 3633 . . . . . . . . 9 ((𝑑 ∈ 𝐿 ∧ (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ 𝑑)) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯))
1916, 18mpan2 689 . . . . . . . 8 (𝑑 ∈ 𝐿 β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯))
2019adantl 482 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯))
21 elfvdm 6928 . . . . . . . . . . 11 (𝐡 ∈ (fBasβ€˜π‘Œ) β†’ π‘Œ ∈ dom fBas)
225, 21syl 17 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ dom fBas)
23 cnvimass 6080 . . . . . . . . . . 11 (◑𝐹 β€œ 𝑑) βŠ† dom 𝐹
24 fmfnfm.f . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:π‘ŒβŸΆπ‘‹)
2523, 24fssdm 6737 . . . . . . . . . 10 (πœ‘ β†’ (◑𝐹 β€œ 𝑑) βŠ† π‘Œ)
2622, 25ssexd 5324 . . . . . . . . 9 (πœ‘ β†’ (◑𝐹 β€œ 𝑑) ∈ V)
2726adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (◑𝐹 β€œ 𝑑) ∈ V)
28 eqid 2732 . . . . . . . . 9 (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) = (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))
2928elrnmpt 5955 . . . . . . . 8 ((◑𝐹 β€œ 𝑑) ∈ V β†’ ((◑𝐹 β€œ 𝑑) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯)))
3027, 29syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ ((◑𝐹 β€œ 𝑑) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ 𝑑) = (◑𝐹 β€œ π‘₯)))
3120, 30mpbird 256 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (◑𝐹 β€œ 𝑑) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
3215, 31sseldd 3983 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (◑𝐹 β€œ 𝑑) ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))))
33 ffun 6720 . . . . . . . 8 (𝐹:π‘ŒβŸΆπ‘‹ β†’ Fun 𝐹)
34 ssid 4004 . . . . . . . 8 (◑𝐹 β€œ 𝑑) βŠ† (◑𝐹 β€œ 𝑑)
35 funimass2 6631 . . . . . . . 8 ((Fun 𝐹 ∧ (◑𝐹 β€œ 𝑑) βŠ† (◑𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
3633, 34, 35sylancl 586 . . . . . . 7 (𝐹:π‘ŒβŸΆπ‘‹ β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
3724, 36syl 17 . . . . . 6 (πœ‘ β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
3837adantr 481 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑)
39 imaeq2 6055 . . . . . . 7 (𝑠 = (◑𝐹 β€œ 𝑑) β†’ (𝐹 β€œ 𝑠) = (𝐹 β€œ (◑𝐹 β€œ 𝑑)))
4039sseq1d 4013 . . . . . 6 (𝑠 = (◑𝐹 β€œ 𝑑) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 ↔ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑))
4140rspcev 3612 . . . . 5 (((◑𝐹 β€œ 𝑑) ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) ∧ (𝐹 β€œ (◑𝐹 β€œ 𝑑)) βŠ† 𝑑) β†’ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)
4232, 38, 41syl2anc 584 . . . 4 ((πœ‘ ∧ 𝑑 ∈ 𝐿) β†’ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)
4342ex 413 . . 3 (πœ‘ β†’ (𝑑 ∈ 𝐿 β†’ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑))
444, 43jcad 513 . 2 (πœ‘ β†’ (𝑑 ∈ 𝐿 β†’ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)))
45 elfiun 9427 . . . . . 6 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∈ V) β†’ (𝑠 ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) ↔ (𝑠 ∈ (fiβ€˜π΅) ∨ 𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∨ βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀))))
465, 9, 45syl2anc 584 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) ↔ (𝑠 ∈ (fiβ€˜π΅) ∨ 𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∨ βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀))))
47 fmfnfm.fm . . . . . . 7 (πœ‘ β†’ ((𝑋 FilMap 𝐹)β€˜π΅) βŠ† 𝐿)
485, 1, 24, 47fmfnfmlem1 23465 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜π΅) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
495, 1, 24, 47fmfnfmlem3 23467 . . . . . . . 8 (πœ‘ β†’ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) = ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
5049eleq2d 2819 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ 𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))
5128elrnmpt 5955 . . . . . . . . 9 (𝑠 ∈ V β†’ (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯)))
5251elv 3480 . . . . . . . 8 (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯))
535, 1, 24, 47fmfnfmlem2 23466 . . . . . . . 8 (πœ‘ β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
5452, 53biimtrid 241 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
5550, 54sylbid 239 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
5649eleq2d 2819 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ 𝑀 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))
5728elrnmpt 5955 . . . . . . . . . . . . 13 (𝑀 ∈ V β†’ (𝑀 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯)))
5857elv 3480 . . . . . . . . . . . 12 (𝑀 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯))
5956, 58bitrdi 286 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯)))
6059adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯)))
61 fbssfi 23348 . . . . . . . . . . . 12 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧)
625, 61sylan 580 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧)
631ad3antrrr 728 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ 𝐿 ∈ (Filβ€˜π‘‹))
641adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ 𝐿 ∈ (Filβ€˜π‘‹))
6547adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ ((𝑋 FilMap 𝐹)β€˜π΅) βŠ† 𝐿)
66 filtop 23366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐿 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐿)
671, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑋 ∈ 𝐿)
6867, 5, 243jca 1128 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑋 ∈ 𝐿 ∧ 𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝐹:π‘ŒβŸΆπ‘‹))
6968adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ (𝑋 ∈ 𝐿 ∧ 𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝐹:π‘ŒβŸΆπ‘‹))
70 ssfg 23383 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐡 ∈ (fBasβ€˜π‘Œ) β†’ 𝐡 βŠ† (π‘ŒfilGen𝐡))
715, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐡 βŠ† (π‘ŒfilGen𝐡))
7271sselda 3982 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 ∈ (π‘ŒfilGen𝐡))
73 eqid 2732 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘ŒfilGen𝐡) = (π‘ŒfilGen𝐡)
7473imaelfm 23462 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋 ∈ 𝐿 ∧ 𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ 𝑠 ∈ (π‘ŒfilGen𝐡)) β†’ (𝐹 β€œ 𝑠) ∈ ((𝑋 FilMap 𝐹)β€˜π΅))
7569, 72, 74syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ (𝐹 β€œ 𝑠) ∈ ((𝑋 FilMap 𝐹)β€˜π΅))
7665, 75sseldd 3983 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ (𝐹 β€œ 𝑠) ∈ 𝐿)
7776adantrr 715 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ (𝐹 β€œ 𝑠) ∈ 𝐿)
7864, 77jca 512 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ (𝐿 ∈ (Filβ€˜π‘‹) ∧ (𝐹 β€œ 𝑠) ∈ 𝐿))
79 filin 23365 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ (𝐹 β€œ 𝑠) ∈ 𝐿 ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
80793expa 1118 . . . . . . . . . . . . . . . . . . 19 (((𝐿 ∈ (Filβ€˜π‘‹) ∧ (𝐹 β€œ 𝑠) ∈ 𝐿) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
8178, 80sylan 580 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
8281adantr 481 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿)
83 simprr 771 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ 𝑑 βŠ† 𝑋)
84 elin 3964 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ((𝐹 β€œ 𝑠) ∩ π‘₯) ↔ (𝑀 ∈ (𝐹 β€œ 𝑠) ∧ 𝑀 ∈ π‘₯))
8524, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ Fun 𝐹)
86 fvelima 6957 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹 ∧ 𝑀 ∈ (𝐹 β€œ 𝑠)) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀)
8786ex 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun 𝐹 β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀))
8885, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀))
8988ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀))
9085ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ Fun 𝐹)
91 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ 𝑠 βŠ† 𝑧)
92 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯)) β†’ 𝑦 ∈ 𝑠)
93 ssel2 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 βŠ† 𝑧 ∧ 𝑦 ∈ 𝑠) β†’ 𝑦 ∈ 𝑧)
9491, 92, 93syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ 𝑦 ∈ 𝑧)
9585ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ Fun 𝐹)
96 fbelss 23344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐡 ∈ (fBasβ€˜π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 βŠ† π‘Œ)
975, 96sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 βŠ† π‘Œ)
9824fdmd 6728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (πœ‘ β†’ dom 𝐹 = π‘Œ)
9998adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ dom 𝐹 = π‘Œ)
10097, 99sseqtrrd 4023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((πœ‘ ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 βŠ† dom 𝐹)
101100adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ 𝑠 βŠ† dom 𝐹)
102101sselda 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ 𝑦 ∈ dom 𝐹)
103 fvimacnv 7054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ ↔ 𝑦 ∈ (◑𝐹 β€œ π‘₯)))
10495, 102, 103syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ ↔ 𝑦 ∈ (◑𝐹 β€œ π‘₯)))
105104biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ β†’ 𝑦 ∈ (◑𝐹 β€œ π‘₯)))
106105impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯)) β†’ 𝑦 ∈ (◑𝐹 β€œ π‘₯))
107106ad2ant2rl 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ 𝑦 ∈ (◑𝐹 β€œ π‘₯))
10894, 107elind 4194 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ 𝑦 ∈ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))
109 inss2 4229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∩ (◑𝐹 β€œ π‘₯)) βŠ† (◑𝐹 β€œ π‘₯)
110 cnvimass 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (◑𝐹 β€œ π‘₯) βŠ† dom 𝐹
111109, 110sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∩ (◑𝐹 β€œ π‘₯)) βŠ† dom 𝐹
112 funfvima2 7235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun 𝐹 ∧ (𝑧 ∩ (◑𝐹 β€œ π‘₯)) βŠ† dom 𝐹) β†’ (𝑦 ∈ (𝑧 ∩ (◑𝐹 β€œ π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
113111, 112mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝐹 β†’ (𝑦 ∈ (𝑧 ∩ (◑𝐹 β€œ π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
11490, 108, 113sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ (𝑑 βŠ† 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯))) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
115114anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) ∧ (𝑦 ∈ 𝑠 ∧ (πΉβ€˜π‘¦) ∈ π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
116115expr 457 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
117 eleq1 2821 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πΉβ€˜π‘¦) = 𝑀 β†’ ((πΉβ€˜π‘¦) ∈ π‘₯ ↔ 𝑀 ∈ π‘₯))
118 eleq1 2821 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πΉβ€˜π‘¦) = 𝑀 β†’ ((πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) ↔ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
119117, 118imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πΉβ€˜π‘¦) = 𝑀 β†’ (((πΉβ€˜π‘¦) ∈ π‘₯ β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))) ↔ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
120116, 119syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) ∧ 𝑦 ∈ 𝑠) β†’ ((πΉβ€˜π‘¦) = 𝑀 β†’ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
121120rexlimdva 3155 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (βˆƒπ‘¦ ∈ 𝑠 (πΉβ€˜π‘¦) = 𝑀 β†’ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
12289, 121syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (𝑀 ∈ (𝐹 β€œ 𝑠) β†’ (𝑀 ∈ π‘₯ β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))))
123122impd 411 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ ((𝑀 ∈ (𝐹 β€œ 𝑠) ∧ 𝑀 ∈ π‘₯) β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
12484, 123biimtrid 241 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ 𝑑 βŠ† 𝑋) β†’ (𝑀 ∈ ((𝐹 β€œ 𝑠) ∩ π‘₯) β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
125124adantrl 714 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ (𝑀 ∈ ((𝐹 β€œ 𝑠) ∩ π‘₯) β†’ 𝑀 ∈ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯)))))
126125ssrdv 3988 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) βŠ† (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
127 simprl 769 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑)
128126, 127sstrd 3992 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ ((𝐹 β€œ 𝑠) ∩ π‘₯) βŠ† 𝑑)
129 filss 23364 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ (((𝐹 β€œ 𝑠) ∩ π‘₯) ∈ 𝐿 ∧ 𝑑 βŠ† 𝑋 ∧ ((𝐹 β€œ 𝑠) ∩ π‘₯) βŠ† 𝑑)) β†’ 𝑑 ∈ 𝐿)
13063, 82, 83, 128, 129syl13anc 1372 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) ∧ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 ∧ 𝑑 βŠ† 𝑋)) β†’ 𝑑 ∈ 𝐿)
131130exp32 421 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))
132 ineq2 4206 . . . . . . . . . . . . . . . . . 18 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ (𝑧 ∩ 𝑀) = (𝑧 ∩ (◑𝐹 β€œ π‘₯)))
133132imaeq2d 6059 . . . . . . . . . . . . . . . . 17 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ (𝐹 β€œ (𝑧 ∩ 𝑀)) = (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))))
134133sseq1d 4013 . . . . . . . . . . . . . . . 16 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 ↔ (𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑))
135134imbi1d 341 . . . . . . . . . . . . . . 15 (𝑀 = (◑𝐹 β€œ π‘₯) β†’ (((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)) ↔ ((𝐹 β€œ (𝑧 ∩ (◑𝐹 β€œ π‘₯))) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
136131, 135syl5ibrcom 246 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) ∧ π‘₯ ∈ 𝐿) β†’ (𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
137136rexlimdva 3155 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑠 ∈ 𝐡 ∧ 𝑠 βŠ† 𝑧)) β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
138137rexlimdvaa 3156 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧 β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))))
139138imp 407 . . . . . . . . . . 11 ((πœ‘ ∧ βˆƒπ‘  ∈ 𝐡 𝑠 βŠ† 𝑧) β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14062, 139syldan 591 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ (βˆƒπ‘₯ ∈ 𝐿 𝑀 = (◑𝐹 β€œ π‘₯) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14160, 140sylbid 239 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (fiβ€˜π΅)) β†’ (𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
142141impr 455 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ 𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))) β†’ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))
143 imaeq2 6055 . . . . . . . . . 10 (𝑠 = (𝑧 ∩ 𝑀) β†’ (𝐹 β€œ 𝑠) = (𝐹 β€œ (𝑧 ∩ 𝑀)))
144143sseq1d 4013 . . . . . . . . 9 (𝑠 = (𝑧 ∩ 𝑀) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 ↔ (𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑))
145144imbi1d 341 . . . . . . . 8 (𝑠 = (𝑧 ∩ 𝑀) β†’ (((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)) ↔ ((𝐹 β€œ (𝑧 ∩ 𝑀)) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
146142, 145syl5ibrcom 246 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ 𝑀 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))) β†’ (𝑠 = (𝑧 ∩ 𝑀) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
147146rexlimdvva 3211 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14848, 55, 1473jaod 1428 . . . . 5 (πœ‘ β†’ ((𝑠 ∈ (fiβ€˜π΅) ∨ 𝑠 ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ∨ βˆƒπ‘§ ∈ (fiβ€˜π΅)βˆƒπ‘€ ∈ (fiβ€˜ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))𝑠 = (𝑧 ∩ 𝑀)) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
14946, 148sylbid 239 . . . 4 (πœ‘ β†’ (𝑠 ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))) β†’ ((𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿))))
150149rexlimdv 3153 . . 3 (πœ‘ β†’ (βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑 β†’ (𝑑 βŠ† 𝑋 β†’ 𝑑 ∈ 𝐿)))
151150impcomd 412 . 2 (πœ‘ β†’ ((𝑑 βŠ† 𝑋 ∧ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑) β†’ 𝑑 ∈ 𝐿))
15244, 151impbid 211 1 (πœ‘ β†’ (𝑑 ∈ 𝐿 ↔ (𝑑 βŠ† 𝑋 ∧ βˆƒπ‘  ∈ (fiβ€˜(𝐡 βˆͺ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))))(𝐹 β€œ 𝑠) βŠ† 𝑑)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  Vcvv 3474   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948   ↦ cmpt 5231  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β€œ cima 5679  Fun wfun 6537  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  ficfi 9407  fBascfbas 20938  filGencfg 20939  Filcfil 23356   FilMap cfm 23444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1o 8468  df-er 8705  df-en 8942  df-fin 8945  df-fi 9408  df-fbas 20947  df-fg 20948  df-fil 23357  df-fm 23449
This theorem is referenced by:  fmfnfm  23469
  Copyright terms: Public domain W3C validator