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

Theorem fmfnfmlem2 21569
 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
fmfnfmlem2 (𝜑 → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
Distinct variable groups:   𝑡,𝑠,𝑥,𝐵   𝐹,𝑠,𝑡,𝑥   𝐿,𝑠,𝑡,𝑥   𝜑,𝑠,𝑡,𝑥   𝑋,𝑠,𝑡,𝑥   𝑌,𝑠,𝑡,𝑥

Proof of Theorem fmfnfmlem2
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmfnfm.l . . . . . 6 (𝜑𝐿 ∈ (Fil‘𝑋))
21ad2antrr 758 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
3 simplr 788 . . . . . 6 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝑥𝐿)
4 fmfnfm.fm . . . . . . . 8 (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
5 fmfnfm.f . . . . . . . . . 10 (𝜑𝐹:𝑌𝑋)
6 ffn 5958 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
7 dffn4 6034 . . . . . . . . . . 11 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
86, 7sylib 207 . . . . . . . . . 10 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
9 foima 6033 . . . . . . . . . 10 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
105, 8, 93syl 18 . . . . . . . . 9 (𝜑 → (𝐹𝑌) = ran 𝐹)
11 filtop 21469 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
121, 11syl 17 . . . . . . . . . 10 (𝜑𝑋𝐿)
13 fmfnfm.b . . . . . . . . . 10 (𝜑𝐵 ∈ (fBas‘𝑌))
14 fgcl 21492 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
15 filtop 21469 . . . . . . . . . . 11 ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
1613, 14, 153syl 18 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑌filGen𝐵))
17 eqid 2610 . . . . . . . . . . 11 (𝑌filGen𝐵) = (𝑌filGen𝐵)
1817imaelfm 21565 . . . . . . . . . 10 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
1912, 13, 5, 16, 18syl31anc 1321 . . . . . . . . 9 (𝜑 → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2010, 19eqeltrrd 2689 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
214, 20sseldd 3569 . . . . . . 7 (𝜑 → ran 𝐹𝐿)
2221ad2antrr 758 . . . . . 6 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ran 𝐹𝐿)
23 filin 21468 . . . . . 6 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
242, 3, 22, 23syl3anc 1318 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
25 simprr 792 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝑡𝑋)
26 elin 3758 . . . . . . 7 (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦𝑥𝑦 ∈ ran 𝐹))
27 fvelrnb 6153 . . . . . . . . . . . . 13 (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
285, 6, 273syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
2928ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
30 ffun 5961 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋 → Fun 𝐹)
315, 30syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → Fun 𝐹)
3231ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → Fun 𝐹)
33 simprr 792 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → 𝑧𝑌)
34 fdm 5964 . . . . . . . . . . . . . . . . . . 19 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
355, 34syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom 𝐹 = 𝑌)
3635ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → dom 𝐹 = 𝑌)
3733, 36eleqtrrd 2691 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → 𝑧 ∈ dom 𝐹)
38 fvimacnv 6240 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
3932, 37, 38syl2anc 691 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
40 cnvimass 5404 . . . . . . . . . . . . . . . . 17 (𝐹𝑥) ⊆ dom 𝐹
41 funfvima2 6397 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → (𝑧 ∈ (𝐹𝑥) → (𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥))))
4232, 40, 41sylancl 693 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → (𝑧 ∈ (𝐹𝑥) → (𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥))))
43 ssel 3562 . . . . . . . . . . . . . . . . 17 ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → ((𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑡))
4443ad2antrl 760 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑡))
4542, 44syld 46 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → (𝑧 ∈ (𝐹𝑥) → (𝐹𝑧) ∈ 𝑡))
4639, 45sylbid 229 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) ∈ 𝑥 → (𝐹𝑧) ∈ 𝑡))
47 eleq1 2676 . . . . . . . . . . . . . . 15 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑥𝑦𝑥))
48 eleq1 2676 . . . . . . . . . . . . . . 15 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑡𝑦𝑡))
4947, 48imbi12d 333 . . . . . . . . . . . . . 14 ((𝐹𝑧) = 𝑦 → (((𝐹𝑧) ∈ 𝑥 → (𝐹𝑧) ∈ 𝑡) ↔ (𝑦𝑥𝑦𝑡)))
5046, 49syl5ibcom 234 . . . . . . . . . . . . 13 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) = 𝑦 → (𝑦𝑥𝑦𝑡)))
5150expr 641 . . . . . . . . . . . 12 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑧𝑌 → ((𝐹𝑧) = 𝑦 → (𝑦𝑥𝑦𝑡))))
5251rexlimdv 3012 . . . . . . . . . . 11 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (∃𝑧𝑌 (𝐹𝑧) = 𝑦 → (𝑦𝑥𝑦𝑡)))
5329, 52sylbid 229 . . . . . . . . . 10 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 → (𝑦𝑥𝑦𝑡)))
5453com23 84 . . . . . . . . 9 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑦𝑥 → (𝑦 ∈ ran 𝐹𝑦𝑡)))
5554impd 446 . . . . . . . 8 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → ((𝑦𝑥𝑦 ∈ ran 𝐹) → 𝑦𝑡))
5655adantrr 749 . . . . . . 7 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝑦𝑥𝑦 ∈ ran 𝐹) → 𝑦𝑡))
5726, 56syl5bi 231 . . . . . 6 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑦 ∈ (𝑥 ∩ ran 𝐹) → 𝑦𝑡))
5857ssrdv 3574 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ 𝑡)
59 filss 21467 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝑥 ∩ ran 𝐹) ∈ 𝐿𝑡𝑋 ∧ (𝑥 ∩ ran 𝐹) ⊆ 𝑡)) → 𝑡𝐿)
602, 24, 25, 58, 59syl13anc 1320 . . . 4 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝑡𝐿)
6160exp32 629 . . 3 ((𝜑𝑥𝐿) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
62 imaeq2 5381 . . . . 5 (𝑠 = (𝐹𝑥) → (𝐹𝑠) = (𝐹 “ (𝐹𝑥)))
6362sseq1d 3595 . . . 4 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡))
6463imbi1d 330 . . 3 (𝑠 = (𝐹𝑥) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
6561, 64syl5ibrcom 236 . 2 ((𝜑𝑥𝐿) → (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
6665rexlimdva 3013 1 (𝜑 → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897   ∩ cin 3539   ⊆ wss 3540  ◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549  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-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-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  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-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-fbas 19564  df-fg 19565  df-fil 21460  df-fm 21552 This theorem is referenced by:  fmfnfmlem4  21571
 Copyright terms: Public domain W3C validator