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

Theorem fmfnfmlem4 21666
Description: Lemma for fmfnfm 21667. (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 21561 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡𝐿) → 𝑡𝑋)
32ex 450 . . . 4 (𝐿 ∈ (Fil‘𝑋) → (𝑡𝐿𝑡𝑋))
41, 3syl 17 . . 3 (𝜑 → (𝑡𝐿𝑡𝑋))
5 fmfnfm.b . . . . . . . . 9 (𝜑𝐵 ∈ (fBas‘𝑌))
6 mptexg 6439 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
7 rnexg 7046 . . . . . . . . . . 11 ((𝑥𝐿 ↦ (𝐹𝑥)) ∈ V → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
86, 7syl 17 . . . . . . . . . 10 (𝐿 ∈ (Fil‘𝑋) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
91, 8syl 17 . . . . . . . . 9 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V)
10 unexg 6913 . . . . . . . . 9 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
115, 9, 10syl2anc 692 . . . . . . . 8 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
12 ssfii 8270 . . . . . . . . 9 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1312unssbd 3774 . . . . . . . 8 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1411, 13syl 17 . . . . . . 7 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
1514adantr 481 . . . . . 6 ((𝜑𝑡𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
16 eqid 2626 . . . . . . . . 9 (𝐹𝑡) = (𝐹𝑡)
17 imaeq2 5425 . . . . . . . . . . 11 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
1817eqeq2d 2636 . . . . . . . . . 10 (𝑥 = 𝑡 → ((𝐹𝑡) = (𝐹𝑥) ↔ (𝐹𝑡) = (𝐹𝑡)))
1918rspcev 3300 . . . . . . . . 9 ((𝑡𝐿 ∧ (𝐹𝑡) = (𝐹𝑡)) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
2016, 19mpan2 706 . . . . . . . 8 (𝑡𝐿 → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
2120adantl 482 . . . . . . 7 ((𝜑𝑡𝐿) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
22 elfvdm 6178 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
235, 22syl 17 . . . . . . . . . 10 (𝜑𝑌 ∈ dom fBas)
24 cnvimass 5448 . . . . . . . . . . 11 (𝐹𝑡) ⊆ dom 𝐹
25 fmfnfm.f . . . . . . . . . . . 12 (𝜑𝐹:𝑌𝑋)
26 fdm 6010 . . . . . . . . . . . 12 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
2725, 26syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝑌)
2824, 27syl5sseq 3637 . . . . . . . . . 10 (𝜑 → (𝐹𝑡) ⊆ 𝑌)
2923, 28ssexd 4770 . . . . . . . . 9 (𝜑 → (𝐹𝑡) ∈ V)
3029adantr 481 . . . . . . . 8 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ V)
31 eqid 2626 . . . . . . . . 9 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
3231elrnmpt 5336 . . . . . . . 8 ((𝐹𝑡) ∈ V → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
3330, 32syl 17 . . . . . . 7 ((𝜑𝑡𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
3421, 33mpbird 247 . . . . . 6 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
3515, 34sseldd 3589 . . . . 5 ((𝜑𝑡𝐿) → (𝐹𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
36 ffun 6007 . . . . . . . 8 (𝐹:𝑌𝑋 → Fun 𝐹)
37 ssid 3608 . . . . . . . 8 (𝐹𝑡) ⊆ (𝐹𝑡)
38 funimass2 5932 . . . . . . . 8 ((Fun 𝐹 ∧ (𝐹𝑡) ⊆ (𝐹𝑡)) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
3936, 37, 38sylancl 693 . . . . . . 7 (𝐹:𝑌𝑋 → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
4025, 39syl 17 . . . . . 6 (𝜑 → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
4140adantr 481 . . . . 5 ((𝜑𝑡𝐿) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
42 imaeq2 5425 . . . . . . 7 (𝑠 = (𝐹𝑡) → (𝐹𝑠) = (𝐹 “ (𝐹𝑡)))
4342sseq1d 3616 . . . . . 6 (𝑠 = (𝐹𝑡) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡))
4443rspcev 3300 . . . . 5 (((𝐹𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∧ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)
4535, 41, 44syl2anc 692 . . . 4 ((𝜑𝑡𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)
4645ex 450 . . 3 (𝜑 → (𝑡𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡))
474, 46jcad 555 . 2 (𝜑 → (𝑡𝐿 → (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
48 elfiun 8281 . . . . . . 7 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ V) → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤))))
495, 9, 48syl2anc 692 . . . . . 6 (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤))))
50 fmfnfm.fm . . . . . . . 8 (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
515, 1, 25, 50fmfnfmlem1 21663 . . . . . . 7 (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
525, 1, 25, 50fmfnfmlem3 21665 . . . . . . . . 9 (𝜑 → (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) = ran (𝑥𝐿 ↦ (𝐹𝑥)))
5352eleq2d 2689 . . . . . . . 8 (𝜑 → (𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))))
54 vex 3194 . . . . . . . . . 10 𝑠 ∈ V
5531elrnmpt 5336 . . . . . . . . . 10 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
5654, 55ax-mp 5 . . . . . . . . 9 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
575, 1, 25, 50fmfnfmlem2 21664 . . . . . . . . 9 (𝜑 → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
5856, 57syl5bi 232 . . . . . . . 8 (𝜑 → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
5953, 58sylbid 230 . . . . . . 7 (𝜑 → (𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
6052eleq2d 2689 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ 𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))))
61 vex 3194 . . . . . . . . . . . . . 14 𝑤 ∈ V
6231elrnmpt 5336 . . . . . . . . . . . . . 14 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
6361, 62ax-mp 5 . . . . . . . . . . . . 13 (𝑤 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥))
6460, 63syl6bb 276 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
6564adantr 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑥𝐿 𝑤 = (𝐹𝑥)))
66 fbssfi 21546 . . . . . . . . . . . . 13 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠𝐵 𝑠𝑧)
675, 66sylan 488 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (fi‘𝐵)) → ∃𝑠𝐵 𝑠𝑧)
681ad3antrrr 765 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
691adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → 𝐿 ∈ (Fil‘𝑋))
7050adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
71 filtop 21564 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
721, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑋𝐿)
7372, 5, 253jca 1240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
7473adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠𝐵) → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
75 ssfg 21581 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
765, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ⊆ (𝑌filGen𝐵))
7776sselda 3588 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
78 eqid 2626 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑌filGen𝐵) = (𝑌filGen𝐵)
7978imaelfm 21660 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
8074, 77, 79syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
8170, 80sseldd 3589 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ 𝐿)
8281adantrr 752 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (𝐹𝑠) ∈ 𝐿)
8369, 82jca 554 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿))
84 filin 21563 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
85843expa 1262 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
8683, 85sylan 488 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
8786adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
88 simprr 795 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝑡𝑋)
89 elin 3779 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹𝑠) ∧ 𝑤𝑥))
9025, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → Fun 𝐹)
91 fvelima 6206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝐹𝑤 ∈ (𝐹𝑠)) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤)
9291ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Fun 𝐹 → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
9390, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
9493ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑤))
9590ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → Fun 𝐹)
96 simplrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → 𝑠𝑧)
97 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → 𝑦𝑠)
98 ssel2 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠𝑧𝑦𝑠) → 𝑦𝑧)
9996, 97, 98syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦𝑧)
10090ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → Fun 𝐹)
101 fbelss 21542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠𝐵) → 𝑠𝑌)
1025, 101sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑠𝐵) → 𝑠𝑌)
10327adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑠𝐵) → dom 𝐹 = 𝑌)
104102, 103sseqtr4d 3626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑠𝐵) → 𝑠 ⊆ dom 𝐹)
105104adantrr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → 𝑠 ⊆ dom 𝐹)
106105sselda 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → 𝑦 ∈ dom 𝐹)
107 fvimacnv 6289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
108100, 106, 107syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
109108biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
110109impr 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → 𝑦 ∈ (𝐹𝑥))
111110ad2ant2rl 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝐹𝑥))
11299, 111elind 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (𝐹𝑥)))
113 inss2 3817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∩ (𝐹𝑥)) ⊆ (𝐹𝑥)
114 cnvimass 5448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐹𝑥) ⊆ dom 𝐹
115113, 114sstri 3597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∩ (𝐹𝑥)) ⊆ dom 𝐹
116 funfvima2 6448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Fun 𝐹 ∧ (𝑧 ∩ (𝐹𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (𝐹𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
117115, 116mpan2 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Fun 𝐹 → (𝑦 ∈ (𝑧 ∩ (𝐹𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
11895, 112, 117sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ (𝑡𝑋 ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥))) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
119118anassrs 679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ (𝑦𝑠 ∧ (𝐹𝑦) ∈ 𝑥)) → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
120119expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
121 eleq1 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑤 → ((𝐹𝑦) ∈ 𝑥𝑤𝑥))
122 eleq1 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑤 → ((𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
123121, 122imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹𝑦) = 𝑤 → (((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))) ↔ (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
124120, 123syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) ∧ 𝑦𝑠) → ((𝐹𝑦) = 𝑤 → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
125124rexlimdva 3029 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (∃𝑦𝑠 (𝐹𝑦) = 𝑤 → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
12694, 125syld 47 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ (𝐹𝑠) → (𝑤𝑥𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))))
127126impd 447 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → ((𝑤 ∈ (𝐹𝑠) ∧ 𝑤𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
12889, 127syl5bi 232 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ 𝑡𝑋) → (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
129128adantrl 751 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → (𝑤 ∈ ((𝐹𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (𝐹𝑥)))))
130129ssrdv 3594 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
131 simprl 793 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡)
132130, 131sstrd 3598 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → ((𝐹𝑠) ∩ 𝑥) ⊆ 𝑡)
133 filss 21562 . . . . . . . . . . . . . . . . . 18 ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹𝑠) ∩ 𝑥) ∈ 𝐿𝑡𝑋 ∧ ((𝐹𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡𝐿)
13468, 87, 88, 132, 133syl13anc 1325 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡𝑡𝑋)) → 𝑡𝐿)
135134exp32 630 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
136 ineq2 3791 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹𝑥) → (𝑧𝑤) = (𝑧 ∩ (𝐹𝑥)))
137136imaeq2d 5429 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹𝑥) → (𝐹 “ (𝑧𝑤)) = (𝐹 “ (𝑧 ∩ (𝐹𝑥))))
138137sseq1d 3616 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡))
139138imbi1d 331 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐹𝑥) → (((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (𝐹𝑥))) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
140135, 139syl5ibrcom 237 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑠𝐵𝑠𝑧)) ∧ 𝑥𝐿) → (𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
141140rexlimdva 3029 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝐵𝑠𝑧)) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
142141rexlimdvaa 3030 . . . . . . . . . . . . 13 (𝜑 → (∃𝑠𝐵 𝑠𝑧 → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))))
143142imp 445 . . . . . . . . . . . 12 ((𝜑 ∧ ∃𝑠𝐵 𝑠𝑧) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14467, 143syldan 487 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (fi‘𝐵)) → (∃𝑥𝐿 𝑤 = (𝐹𝑥) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
14565, 144sylbid 230 . . . . . . . . . 10 ((𝜑𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
146145impr 648 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
147 imaeq2 5425 . . . . . . . . . . 11 (𝑠 = (𝑧𝑤) → (𝐹𝑠) = (𝐹 “ (𝑧𝑤)))
148147sseq1d 3616 . . . . . . . . . 10 (𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧𝑤)) ⊆ 𝑡))
149148imbi1d 331 . . . . . . . . 9 (𝑠 = (𝑧𝑤) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝑧𝑤)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
150146, 149syl5ibrcom 237 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
151150rexlimdvva 3036 . . . . . . 7 (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
15251, 59, 1513jaod 1389 . . . . . 6 (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥𝐿 ↦ (𝐹𝑥)))𝑠 = (𝑧𝑤)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
15349, 152sylbid 230 . . . . 5 (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
154153rexlimdv 3028 . . . 4 (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
155154com23 86 . . 3 (𝜑 → (𝑡𝑋 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡𝑡𝐿)))
156155impd 447 . 2 (𝜑 → ((𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡) → 𝑡𝐿))
15747, 156impbid 202 1 (𝜑 → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3o 1035  w3a 1036   = wceq 1480  wcel 1992  wrex 2913  Vcvv 3191  cun 3558  cin 3559  wss 3560  cmpt 4678  ccnv 5078  dom cdm 5079  ran crn 5080  cima 5082  Fun wfun 5844  wf 5846  cfv 5850  (class class class)co 6605  ficfi 8261  fBascfbas 19648  filGencfg 19649  Filcfil 21554   FilMap cfm 21642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-oadd 7510  df-er 7688  df-en 7901  df-fin 7904  df-fi 8262  df-fbas 19657  df-fg 19658  df-fil 21555  df-fm 21647
This theorem is referenced by:  fmfnfm  21667
  Copyright terms: Public domain W3C validator