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

Theorem fmfnfmlem4 21571
 Description: Lemma for fmfnfm 21572. (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 21466 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡𝐿) → 𝑡𝑋)
32ex 449 . . . 4 (𝐿 ∈ (Fil‘𝑋) → (𝑡𝐿𝑡𝑋))
41, 3syl 17 . . 3 (𝜑 → (𝑡𝐿𝑡𝑋))
5 fmfnfm.b . . . . . . . . 9 (𝜑𝐵 ∈ (fBas‘𝑌))
6 mptexg 6389 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
7 rnexg 6990 . . . . . . . . . . 11 ((𝑥𝐿 ↦ (𝐹𝑥)) ∈ V → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
86, 7syl 17 . . . . . . . . . 10 (𝐿 ∈ (Fil‘𝑋) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
91, 8syl 17 . . . . . . . . 9 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
10 unexg 6857 . . . . . . . . 9 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
115, 9, 10syl2anc 691 . . . . . . . 8 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
12 ssfii 8208 . . . . . . . . 9 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1312unssbd 3753 . . . . . . . 8 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1411, 13syl 17 . . . . . . 7 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1514adantr 480 . . . . . 6 ((𝜑𝑡𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
16 eqid 2610 . . . . . . . . 9 (𝐹𝑡) = (𝐹𝑡)
17 imaeq2 5381 . . . . . . . . . . 11 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
1817eqeq2d 2620 . . . . . . . . . 10 (𝑥 = 𝑡 → ((𝐹𝑡) = (𝐹𝑥) ↔ (𝐹𝑡) = (𝐹𝑡)))
1918rspcev 3282 . . . . . . . . 9 ((𝑡𝐿 ∧ (𝐹𝑡) = (𝐹𝑡)) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
2016, 19mpan2 703 . . . . . . . 8 (𝑡𝐿 → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
2120adantl 481 . . . . . . 7 ((𝜑𝑡𝐿) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
22 elfvdm 6130 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
235, 22syl 17 . . . . . . . . . 10 (𝜑𝑌 ∈ dom fBas)
24 cnvimass 5404 . . . . . . . . . . 11 (𝐹𝑡) ⊆ dom 𝐹
25 fmfnfm.f . . . . . . . . . . . 12 (𝜑𝐹:𝑌𝑋)
26 fdm 5964 . . . . . . . . . . . 12 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
2725, 26syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝑌)
2824, 27syl5sseq 3616 . . . . . . . . . 10 (𝜑 → (𝐹𝑡) ⊆ 𝑌)
2923, 28ssexd 4733 . . . . . . . . 9 (𝜑 → (𝐹𝑡) ∈ V)
3029adantr 480 . . . . . . . 8 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ V)
31 eqid 2610 . . . . . . . . 9 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
3231elrnmpt 5293 . . . . . . . 8 ((𝐹𝑡) ∈ V → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
3330, 32syl 17 . . . . . . 7 ((𝜑𝑡𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
3421, 33mpbird 246 . . . . . 6 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
3515, 34sseldd 3569 . . . . 5 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
36 ffun 5961 . . . . . . . 8 (𝐹:𝑌𝑋 → Fun 𝐹)
37 ssid 3587 . . . . . . . 8 (𝐹𝑡) ⊆ (𝐹𝑡)
38 funimass2 5886 . . . . . . . 8 ((Fun 𝐹 ∧ (𝐹𝑡) ⊆ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
3936, 37, 38sylancl 693 . . . . . . 7 (𝐹:𝑌𝑋 → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
4025, 39syl 17 . . . . . 6 (𝜑 → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
4140adantr 480 . . . . 5 ((𝜑𝑡𝐿) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
42 imaeq2 5381 . . . . . . 7 (𝑠 = (𝐹𝑡) → (𝐹𝑠) = (𝐹 “ (𝐹𝑡)))
4342sseq1d 3595 . . . . . 6 (𝑠 = (𝐹𝑡) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡))
4443rspcev 3282 . . . . 5 (((𝐹𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∧ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)
4535, 41, 44syl2anc 691 . . . 4 ((𝜑𝑡𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)
4645ex 449 . . 3 (𝜑 → (𝑡𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡))
474, 46jcad 554 . 2 (𝜑 → (𝑡𝐿 → (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
48 elfiun 8219 . . . . . . 7 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V) → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤))))
495, 9, 48syl2anc 691 . . . . . 6 (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤))))
50 fmfnfm.fm . . . . . . . 8 (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
515, 1, 25, 50fmfnfmlem1 21568 . . . . . . 7 (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
525, 1, 25, 50fmfnfmlem3 21570 . . . . . . . . 9 (𝜑 → (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) = ran (𝑥𝐿 ↦ (𝐹𝑥)))
5352eleq2d 2673 . . . . . . . 8 (𝜑 → (𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))))
54 vex 3176 . . . . . . . . . 10 𝑠 ∈ V
5531elrnmpt 5293 . . . . . . . . . 10 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
5654, 55ax-mp 5 . . . . . . . . 9 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
575, 1, 25, 50fmfnfmlem2 21569 . . . . . . . . 9 (𝜑 → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
5856, 57syl5bi 231 . . . . . . . 8 (𝜑 → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
5953, 58sylbid 229 . . . . . . 7 (𝜑 → (𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
6052eleq2d 2673 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ 𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))))
61 vex 3176 . . . . . . . . . . . . . 14 𝑤 ∈ V
6231elrnmpt 5293 . . . . . . . . . . . . . 14 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
6361, 62ax-mp 5 . . . . . . . . . . . . 13 (𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥))
6460, 63syl6bb 275 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
6564adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
66 fbssfi 21451 . . . . . . . . . . . . 13 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠𝐵 𝑠𝑧)
675, 66sylan 487 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (fi‘𝐵)) → ∃𝑠𝐵 𝑠𝑧)
681ad3antrrr 762 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
691adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → 𝐿 ∈ (Fil‘𝑋))
7050adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
71 filtop 21469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
721, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑋𝐿)
7372, 5, 253jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
7473adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠𝐵) → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
75 ssfg 21486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
765, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ⊆ (𝑌filGen𝐵))
7776sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
78 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑌filGen𝐵) = (𝑌filGen𝐵)
7978imaelfm 21565 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
8074, 77, 79syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
8170, 80sseldd 3569 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ 𝐿)
8281adantrr 749 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (𝐹𝑠) ∈ 𝐿)
8369, 82jca 553 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿))
84 filin 21468 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
85843expa 1257 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
8683, 85sylan 487 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
8786adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
88 simprr 792 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝑡𝑋)
89 elin 3758 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹𝑠) ∧ 𝑤𝑥))
9025, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → Fun 𝐹)
91 fvelima 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝐹𝑤 ∈ (𝐹𝑠)) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤)
9291ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Fun 𝐹 → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
9390, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
9493ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
9590ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → Fun 𝐹)
96 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → 𝑠𝑧)
97 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → 𝑦𝑠)
98 ssel2 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠𝑧𝑦𝑠) → 𝑦𝑧)
9996, 97, 98syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦𝑧)
10090ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → Fun 𝐹)
101 fbelss 21447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠𝐵) → 𝑠𝑌)
1025, 101sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑠𝐵) → 𝑠𝑌)
10327adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑠𝐵) → dom 𝐹 = 𝑌)
104102, 103sseqtr4d 3605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑠𝐵) → 𝑠 ⊆ dom 𝐹)
105104adantrr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → 𝑠 ⊆ dom 𝐹)
106105sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → 𝑦 ∈ dom 𝐹)
107 fvimacnv 6240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
108100, 106, 107syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
109108biimpd 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
110109impr 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → 𝑦 ∈ (𝐹𝑥))
111110ad2ant2rl 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝐹𝑥))
11299, 111elind 3760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (𝐹𝑥)))
113 inss2 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∩ (𝐹𝑥)) ⊆ (𝐹𝑥)
114 cnvimass 5404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐹𝑥) ⊆ dom 𝐹
115113, 114sstri 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∩ (𝐹𝑥)) ⊆ dom 𝐹
116 funfvima2 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Fun 𝐹 ∧ (𝑧 ∩ (𝐹𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (𝐹𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
117115, 116mpan2 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Fun 𝐹 → (𝑦 ∈ (𝑧 ∩ (𝐹𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
11895, 112, 117sylc 63 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
119118anassrs 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
120119expr 641 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
121 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑤 → ((𝐹𝑦) ∈ 𝑥𝑤𝑥))
122 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑤 → ((𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
123121, 122imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹𝑦) = 𝑤 → (((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))) ↔ (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
124120, 123syl5ibcom 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ 𝑦𝑠) → ((𝐹𝑦) = 𝑤 → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
125124rexlimdva 3013 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (∃𝑦𝑠 (𝐹𝑦) = 𝑤 → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
12694, 125syld 46 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ (𝐹𝑠) → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
127126impd 446 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → ((𝑤 ∈ (𝐹𝑠) ∧ 𝑤𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
12889, 127syl5bi 231 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
129128adantrl 748 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
130129ssrdv 3574 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
131 simprl 790 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡)
132130, 131sstrd 3578 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ⊆ 𝑡)
133 filss 21467 . . . . . . . . . . . . . . . . . 18 ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹𝑠) ∩ 𝑥) ∈ 𝐿𝑡𝑋 ∧ ((𝐹𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡𝐿)
13468, 87, 88, 132, 133syl13anc 1320 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝑡𝐿)
135134exp32 629 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
136 ineq2 3770 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹𝑥) → (𝑧𝑤) = (𝑧 ∩ (𝐹𝑥)))
137136imaeq2d 5385 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹𝑥) → (𝐹 “ (𝑧𝑤)) = (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
138137sseq1d 3595 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡))
139138imbi1d 330 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐹𝑥) → (((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
140135, 139syl5ibrcom 236 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → (𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
141140rexlimdva 3013 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
142141rexlimdvaa 3014 . . . . . . . . . . . . 13 (𝜑 → (∃𝑠𝐵 𝑠𝑧 → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))))
143142imp 444 . . . . . . . . . . . 12 ((𝜑 ∧ ∃𝑠𝐵 𝑠𝑧) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14467, 143syldan 486 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (fi‘𝐵)) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14565, 144sylbid 229 . . . . . . . . . 10 ((𝜑𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
146145impr 647 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
147 imaeq2 5381 . . . . . . . . . . 11 (𝑠 = (𝑧𝑤) → (𝐹𝑠) = (𝐹 “ (𝑧𝑤)))
148147sseq1d 3595 . . . . . . . . . 10 (𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧𝑤)) ⊆ 𝑡))
149148imbi1d 330 . . . . . . . . 9 (𝑠 = (𝑧𝑤) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
150146, 149syl5ibrcom 236 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
151150rexlimdvva 3020 . . . . . . 7 (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
15251, 59, 1513jaod 1384 . . . . . 6 (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
15349, 152sylbid 229 . . . . 5 (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
154153rexlimdv 3012 . . . 4 (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
155154com23 84 . . 3 (𝜑 → (𝑡𝑋 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡𝑡𝐿)))
156155impd 446 . 2 (𝜑 → ((𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡) → 𝑡𝐿))
15747, 156impbid 201 1 (𝜑 → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540   ↦ cmpt 4643  ◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041  Fun wfun 5798  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ficfi 8199  fBascfbas 19555  filGencfg 19556  Filcfil 21459   FilMap cfm 21547 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845  df-fi 8200  df-fbas 19564  df-fg 19565  df-fil 21460  df-fm 21552 This theorem is referenced by:  fmfnfm  21572
 Copyright terms: Public domain W3C validator