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

Theorem fmfnfmlem4 23965
Description: Lemma for fmfnfm 23966. (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 23860 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡𝐿) → 𝑡𝑋)
32ex 412 . . . 4 (𝐿 ∈ (Fil‘𝑋) → (𝑡𝐿𝑡𝑋))
41, 3syl 17 . . 3 (𝜑 → (𝑡𝐿𝑡𝑋))
5 fmfnfm.b . . . . . . . . 9 (𝜑𝐵 ∈ (fBas‘𝑌))
6 mptexg 7241 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
7 rnexg 7924 . . . . . . . . . . 11 ((𝑥𝐿 ↦ (𝐹𝑥)) ∈ V → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
86, 7syl 17 . . . . . . . . . 10 (𝐿 ∈ (Fil‘𝑋) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
91, 8syl 17 . . . . . . . . 9 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
10 unexg 7763 . . . . . . . . 9 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
115, 9, 10syl2anc 584 . . . . . . . 8 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
12 ssfii 9459 . . . . . . . . 9 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1312unssbd 4194 . . . . . . . 8 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1411, 13syl 17 . . . . . . 7 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1514adantr 480 . . . . . 6 ((𝜑𝑡𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
16 eqid 2737 . . . . . . . . 9 (𝐹𝑡) = (𝐹𝑡)
17 imaeq2 6074 . . . . . . . . . 10 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
1817rspceeqv 3645 . . . . . . . . 9 ((𝑡𝐿 ∧ (𝐹𝑡) = (𝐹𝑡)) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
1916, 18mpan2 691 . . . . . . . 8 (𝑡𝐿 → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
2019adantl 481 . . . . . . 7 ((𝜑𝑡𝐿) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
21 elfvdm 6943 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
225, 21syl 17 . . . . . . . . . 10 (𝜑𝑌 ∈ dom fBas)
23 cnvimass 6100 . . . . . . . . . . 11 (𝐹𝑡) ⊆ dom 𝐹
24 fmfnfm.f . . . . . . . . . . 11 (𝜑𝐹:𝑌𝑋)
2523, 24fssdm 6755 . . . . . . . . . 10 (𝜑 → (𝐹𝑡) ⊆ 𝑌)
2622, 25ssexd 5324 . . . . . . . . 9 (𝜑 → (𝐹𝑡) ∈ V)
2726adantr 480 . . . . . . . 8 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ V)
28 eqid 2737 . . . . . . . . 9 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
2928elrnmpt 5969 . . . . . . . 8 ((𝐹𝑡) ∈ V → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
3027, 29syl 17 . . . . . . 7 ((𝜑𝑡𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
3120, 30mpbird 257 . . . . . 6 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
3215, 31sseldd 3984 . . . . 5 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
33 ffun 6739 . . . . . . . 8 (𝐹:𝑌𝑋 → Fun 𝐹)
34 ssid 4006 . . . . . . . 8 (𝐹𝑡) ⊆ (𝐹𝑡)
35 funimass2 6649 . . . . . . . 8 ((Fun 𝐹 ∧ (𝐹𝑡) ⊆ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
3633, 34, 35sylancl 586 . . . . . . 7 (𝐹:𝑌𝑋 → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
3724, 36syl 17 . . . . . 6 (𝜑 → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
3837adantr 480 . . . . 5 ((𝜑𝑡𝐿) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
39 imaeq2 6074 . . . . . . 7 (𝑠 = (𝐹𝑡) → (𝐹𝑠) = (𝐹 “ (𝐹𝑡)))
4039sseq1d 4015 . . . . . 6 (𝑠 = (𝐹𝑡) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡))
4140rspcev 3622 . . . . 5 (((𝐹𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∧ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)
4232, 38, 41syl2anc 584 . . . 4 ((𝜑𝑡𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)
4342ex 412 . . 3 (𝜑 → (𝑡𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡))
444, 43jcad 512 . 2 (𝜑 → (𝑡𝐿 → (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
45 elfiun 9470 . . . . . 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 23962 . . . . . 6 (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
495, 1, 24, 47fmfnfmlem3 23964 . . . . . . . 8 (𝜑 → (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) = ran (𝑥𝐿 ↦ (𝐹𝑥)))
5049eleq2d 2827 . . . . . . 7 (𝜑 → (𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))))
5128elrnmpt 5969 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
5251elv 3485 . . . . . . . 8 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
535, 1, 24, 47fmfnfmlem2 23963 . . . . . . . 8 (𝜑 → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
5452, 53biimtrid 242 . . . . . . 7 (𝜑 → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
5550, 54sylbid 240 . . . . . 6 (𝜑 → (𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
5649eleq2d 2827 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ 𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))))
5728elrnmpt 5969 . . . . . . . . . . . . 13 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
5857elv 3485 . . . . . . . . . . . 12 (𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥))
5956, 58bitrdi 287 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
6059adantr 480 . . . . . . . . . 10 ((𝜑𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
61 fbssfi 23845 . . . . . . . . . . . 12 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠𝐵 𝑠𝑧)
625, 61sylan 580 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (fi‘𝐵)) → ∃𝑠𝐵 𝑠𝑧)
631ad3antrrr 730 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
641adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → 𝐿 ∈ (Fil‘𝑋))
6547adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
66 filtop 23863 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
671, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑋𝐿)
6867, 5, 243jca 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
6968adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
70 ssfg 23880 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
715, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 ⊆ (𝑌filGen𝐵))
7271sselda 3983 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
73 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑌filGen𝐵) = (𝑌filGen𝐵)
7473imaelfm 23959 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
7569, 72, 74syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
7665, 75sseldd 3984 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ 𝐿)
7776adantrr 717 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (𝐹𝑠) ∈ 𝐿)
7864, 77jca 511 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿))
79 filin 23862 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
80793expa 1119 . . . . . . . . . . . . . . . . . . 19 (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
8178, 80sylan 580 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
8281adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
83 simprr 773 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝑡𝑋)
84 elin 3967 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹𝑠) ∧ 𝑤𝑥))
8524, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → Fun 𝐹)
86 fvelima 6974 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹𝑤 ∈ (𝐹𝑠)) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤)
8786ex 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun 𝐹 → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
8885, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
8988ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
9085ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → Fun 𝐹)
91 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → 𝑠𝑧)
92 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → 𝑦𝑠)
93 ssel2 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠𝑧𝑦𝑠) → 𝑦𝑧)
9491, 92, 93syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦𝑧)
9585ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → Fun 𝐹)
96 fbelss 23841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠𝐵) → 𝑠𝑌)
975, 96sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑠𝐵) → 𝑠𝑌)
9824fdmd 6746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → dom 𝐹 = 𝑌)
9998adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑠𝐵) → dom 𝐹 = 𝑌)
10097, 99sseqtrrd 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑠𝐵) → 𝑠 ⊆ dom 𝐹)
101100adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → 𝑠 ⊆ dom 𝐹)
102101sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → 𝑦 ∈ dom 𝐹)
103 fvimacnv 7073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
10495, 102, 103syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
105104biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
106105impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → 𝑦 ∈ (𝐹𝑥))
107106ad2ant2rl 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝐹𝑥))
10894, 107elind 4200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (𝐹𝑥)))
109 inss2 4238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∩ (𝐹𝑥)) ⊆ (𝐹𝑥)
110 cnvimass 6100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹𝑥) ⊆ dom 𝐹
111109, 110sstri 3993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∩ (𝐹𝑥)) ⊆ dom 𝐹
112 funfvima2 7251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun 𝐹 ∧ (𝑧 ∩ (𝐹𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (𝐹𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
113111, 112mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝐹 → (𝑦 ∈ (𝑧 ∩ (𝐹𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
11490, 108, 113sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
115114anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
116115expr 456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
117 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹𝑦) = 𝑤 → ((𝐹𝑦) ∈ 𝑥𝑤𝑥))
118 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹𝑦) = 𝑤 → ((𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
119117, 118imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑦) = 𝑤 → (((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))) ↔ (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
120116, 119syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ 𝑦𝑠) → ((𝐹𝑦) = 𝑤 → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
121120rexlimdva 3155 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (∃𝑦𝑠 (𝐹𝑦) = 𝑤 → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
12289, 121syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ (𝐹𝑠) → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
123122impd 410 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → ((𝑤 ∈ (𝐹𝑠) ∧ 𝑤𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
12484, 123biimtrid 242 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
125124adantrl 716 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
126125ssrdv 3989 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
127 simprl 771 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡)
128126, 127sstrd 3994 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ⊆ 𝑡)
129 filss 23861 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹𝑠) ∩ 𝑥) ∈ 𝐿𝑡𝑋 ∧ ((𝐹𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡𝐿)
13063, 82, 83, 128, 129syl13anc 1374 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝑡𝐿)
131130exp32 420 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
132 ineq2 4214 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹𝑥) → (𝑧𝑤) = (𝑧 ∩ (𝐹𝑥)))
133132imaeq2d 6078 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹𝑥) → (𝐹 “ (𝑧𝑤)) = (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
134133sseq1d 4015 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡))
135134imbi1d 341 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝑥) → (((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
136131, 135syl5ibrcom 247 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → (𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
137136rexlimdva 3155 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
138137rexlimdvaa 3156 . . . . . . . . . . . 12 (𝜑 → (∃𝑠𝐵 𝑠𝑧 → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))))
139138imp 406 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑠𝐵 𝑠𝑧) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14062, 139syldan 591 . . . . . . . . . 10 ((𝜑𝑧 ∈ (fi‘𝐵)) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14160, 140sylbid 240 . . . . . . . . 9 ((𝜑𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
142141impr 454 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
143 imaeq2 6074 . . . . . . . . . 10 (𝑠 = (𝑧𝑤) → (𝐹𝑠) = (𝐹 “ (𝑧𝑤)))
144143sseq1d 4015 . . . . . . . . 9 (𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧𝑤)) ⊆ 𝑡))
145144imbi1d 341 . . . . . . . 8 (𝑠 = (𝑧𝑤) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
146142, 145syl5ibrcom 247 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
147146rexlimdvva 3213 . . . . . 6 (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14848, 55, 1473jaod 1431 . . . . 5 (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14946, 148sylbid 240 . . . 4 (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
150149rexlimdv 3153 . . 3 (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
151150impcomd 411 . 2 (𝜑 → ((𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡) → 𝑡𝐿))
15244, 151impbid 212 1 (𝜑 → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3o 1086  w3a 1087   = wceq 1540  wcel 2108  wrex 3070  Vcvv 3480  cun 3949  cin 3950  wss 3951  cmpt 5225  ccnv 5684  dom cdm 5685  ran crn 5686  cima 5688  Fun wfun 6555  wf 6557  cfv 6561  (class class class)co 7431  ficfi 9450  fBascfbas 21352  filGencfg 21353  Filcfil 23853   FilMap cfm 23941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1o 8506  df-2o 8507  df-en 8986  df-fin 8989  df-fi 9451  df-fbas 21361  df-fg 21362  df-fil 23854  df-fm 23946
This theorem is referenced by:  fmfnfm  23966
  Copyright terms: Public domain W3C validator