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

Theorem fmfnfmlem2 21881
Description: Lemma for fmfnfm 21884. (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 764 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
3 simplr 809 . . . . . 6 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝑥𝐿)
4 fmfnfm.fm . . . . . . . 8 (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
5 fmfnfm.f . . . . . . . . . 10 (𝜑𝐹:𝑌𝑋)
6 ffn 6158 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
7 dffn4 6234 . . . . . . . . . . 11 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
86, 7sylib 208 . . . . . . . . . 10 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
9 foima 6233 . . . . . . . . . 10 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
105, 8, 93syl 18 . . . . . . . . 9 (𝜑 → (𝐹𝑌) = ran 𝐹)
11 filtop 21781 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
121, 11syl 17 . . . . . . . . . 10 (𝜑𝑋𝐿)
13 fmfnfm.b . . . . . . . . . 10 (𝜑𝐵 ∈ (fBas‘𝑌))
14 fgcl 21804 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
15 filtop 21781 . . . . . . . . . . 11 ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
1613, 14, 153syl 18 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑌filGen𝐵))
17 eqid 2724 . . . . . . . . . . 11 (𝑌filGen𝐵) = (𝑌filGen𝐵)
1817imaelfm 21877 . . . . . . . . . 10 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
1912, 13, 5, 16, 18syl31anc 1442 . . . . . . . . 9 (𝜑 → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2010, 19eqeltrrd 2804 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
214, 20sseldd 3710 . . . . . . 7 (𝜑 → ran 𝐹𝐿)
2221ad2antrr 764 . . . . . 6 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ran 𝐹𝐿)
23 filin 21780 . . . . . 6 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
242, 3, 22, 23syl3anc 1439 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
25 simprr 813 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝑡𝑋)
26 elin 3904 . . . . . . 7 (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦𝑥𝑦 ∈ ran 𝐹))
27 fvelrnb 6357 . . . . . . . . . . . . 13 (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
285, 6, 273syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
2928ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
30 ffun 6161 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋 → Fun 𝐹)
315, 30syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → Fun 𝐹)
3231ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → Fun 𝐹)
33 simprr 813 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → 𝑧𝑌)
34 fdm 6164 . . . . . . . . . . . . . . . . . . 19 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
355, 34syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom 𝐹 = 𝑌)
3635ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → dom 𝐹 = 𝑌)
3733, 36eleqtrrd 2806 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → 𝑧 ∈ dom 𝐹)
38 fvimacnv 6447 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
3932, 37, 38syl2anc 696 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
40 cnvimass 5595 . . . . . . . . . . . . . . . . 17 (𝐹𝑥) ⊆ dom 𝐹
41 funfvima2 6608 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → (𝑧 ∈ (𝐹𝑥) → (𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥))))
4232, 40, 41sylancl 697 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → (𝑧 ∈ (𝐹𝑥) → (𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥))))
43 ssel 3703 . . . . . . . . . . . . . . . . 17 ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → ((𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑡))
4443ad2antrl 766 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) ∈ (𝐹 “ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑡))
4542, 44syld 47 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → (𝑧 ∈ (𝐹𝑥) → (𝐹𝑧) ∈ 𝑡))
4639, 45sylbid 230 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) ∈ 𝑥 → (𝐹𝑧) ∈ 𝑡))
47 eleq1 2791 . . . . . . . . . . . . . . 15 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑥𝑦𝑥))
48 eleq1 2791 . . . . . . . . . . . . . . 15 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑡𝑦𝑡))
4947, 48imbi12d 333 . . . . . . . . . . . . . 14 ((𝐹𝑧) = 𝑦 → (((𝐹𝑧) ∈ 𝑥 → (𝐹𝑧) ∈ 𝑡) ↔ (𝑦𝑥𝑦𝑡)))
5046, 49syl5ibcom 235 . . . . . . . . . . . . 13 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑧𝑌)) → ((𝐹𝑧) = 𝑦 → (𝑦𝑥𝑦𝑡)))
5150expr 644 . . . . . . . . . . . 12 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑧𝑌 → ((𝐹𝑧) = 𝑦 → (𝑦𝑥𝑦𝑡))))
5251rexlimdv 3132 . . . . . . . . . . 11 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (∃𝑧𝑌 (𝐹𝑧) = 𝑦 → (𝑦𝑥𝑦𝑡)))
5329, 52sylbid 230 . . . . . . . . . 10 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 → (𝑦𝑥𝑦𝑡)))
5453com23 86 . . . . . . . . 9 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → (𝑦𝑥 → (𝑦 ∈ ran 𝐹𝑦𝑡)))
5554impd 446 . . . . . . . 8 (((𝜑𝑥𝐿) ∧ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡) → ((𝑦𝑥𝑦 ∈ ran 𝐹) → 𝑦𝑡))
5655adantrr 755 . . . . . . 7 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝑦𝑥𝑦 ∈ ran 𝐹) → 𝑦𝑡))
5726, 56syl5bi 232 . . . . . 6 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑦 ∈ (𝑥 ∩ ran 𝐹) → 𝑦𝑡))
5857ssrdv 3715 . . . . 5 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ 𝑡)
59 filss 21779 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝑥 ∩ ran 𝐹) ∈ 𝐿𝑡𝑋 ∧ (𝑥 ∩ ran 𝐹) ⊆ 𝑡)) → 𝑡𝐿)
602, 24, 25, 58, 59syl13anc 1441 . . . 4 (((𝜑𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → 𝑡𝐿)
6160exp32 632 . . 3 ((𝜑𝑥𝐿) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
62 imaeq2 5572 . . . . 5 (𝑠 = (𝐹𝑥) → (𝐹𝑠) = (𝐹 “ (𝐹𝑥)))
6362sseq1d 3738 . . . 4 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡))
6463imbi1d 330 . . 3 (𝑠 = (𝐹𝑥) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)) ↔ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
6561, 64syl5ibrcom 237 . 2 ((𝜑𝑥𝐿) → (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
6665rexlimdva 3133 1 (𝜑 → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wcel 2103  wrex 3015  cin 3679  wss 3680  ccnv 5217  dom cdm 5218  ran crn 5219  cima 5221  Fun wfun 5995   Fn wfn 5996  wf 5997  ontowfo 5999  cfv 6001  (class class class)co 6765  fBascfbas 19857  filGencfg 19858  Filcfil 21771   FilMap cfm 21859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-fbas 19866  df-fg 19867  df-fil 21772  df-fm 21864
This theorem is referenced by:  fmfnfmlem4  21883
  Copyright terms: Public domain W3C validator