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

Theorem elfm3 21955
Description: An alternate formulation of elementhood in a mapping filter that requires 𝐹 to be onto. (Contributed by Jeff Hankins, 1-Oct-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
Hypothesis
Ref Expression
elfm2.l 𝐿 = (𝑌filGen𝐵)
Assertion
Ref Expression
elfm3 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
Distinct variable groups:   𝑥,𝐵   𝑥,𝐹   𝑥,𝑋   𝑥,𝐴   𝑥,𝐿   𝑥,𝑌

Proof of Theorem elfm3
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 foima 6281 . . . 4 (𝐹:𝑌onto𝑋 → (𝐹𝑌) = 𝑋)
21adantl 473 . . 3 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝑌) = 𝑋)
3 fofun 6277 . . . 4 (𝐹:𝑌onto𝑋 → Fun 𝐹)
4 elfvdm 6381 . . . 4 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
5 funimaexg 6136 . . . 4 ((Fun 𝐹𝑌 ∈ dom fBas) → (𝐹𝑌) ∈ V)
63, 4, 5syl2anr 496 . . 3 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝑌) ∈ V)
72, 6eqeltrrd 2840 . 2 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → 𝑋 ∈ V)
8 fof 6276 . . . . 5 (𝐹:𝑌onto𝑋𝐹:𝑌𝑋)
9 elfm2.l . . . . . 6 𝐿 = (𝑌filGen𝐵)
109elfm2 21953 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
118, 10syl3an3 1170 . . . 4 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
12 fgcl 21883 . . . . . . . . . . . 12 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
139, 12syl5eqel 2843 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → 𝐿 ∈ (Fil‘𝑌))
14133ad2ant2 1129 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → 𝐿 ∈ (Fil‘𝑌))
1514ad2antrr 764 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝐿 ∈ (Fil‘𝑌))
16 simprl 811 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝑦𝐿)
17 cnvimass 5643 . . . . . . . . . . . 12 (𝐹𝐴) ⊆ dom 𝐹
18 fofn 6278 . . . . . . . . . . . . 13 (𝐹:𝑌onto𝑋𝐹 Fn 𝑌)
19 fndm 6151 . . . . . . . . . . . . 13 (𝐹 Fn 𝑌 → dom 𝐹 = 𝑌)
2018, 19syl 17 . . . . . . . . . . . 12 (𝐹:𝑌onto𝑋 → dom 𝐹 = 𝑌)
2117, 20syl5sseq 3794 . . . . . . . . . . 11 (𝐹:𝑌onto𝑋 → (𝐹𝐴) ⊆ 𝑌)
22213ad2ant3 1130 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝐴) ⊆ 𝑌)
2322ad2antrr 764 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → (𝐹𝐴) ⊆ 𝑌)
2433ad2ant3 1130 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → Fun 𝐹)
2524ad2antrr 764 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → Fun 𝐹)
269eleq2i 2831 . . . . . . . . . . . . . . 15 (𝑦𝐿𝑦 ∈ (𝑌filGen𝐵))
27 elfg 21876 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (fBas‘𝑌) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
28273ad2ant2 1129 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
2928adantr 472 . . . . . . . . . . . . . . 15 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
3026, 29syl5bb 272 . . . . . . . . . . . . . 14 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (𝑦𝐿 ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
3130simprbda 654 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → 𝑦𝑌)
32 sseq2 3768 . . . . . . . . . . . . . . . . 17 (dom 𝐹 = 𝑌 → (𝑦 ⊆ dom 𝐹𝑦𝑌))
3332biimpar 503 . . . . . . . . . . . . . . . 16 ((dom 𝐹 = 𝑌𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3420, 33sylan 489 . . . . . . . . . . . . . . 15 ((𝐹:𝑌onto𝑋𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
35343ad2antl3 1203 . . . . . . . . . . . . . 14 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3635adantlr 753 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3731, 36syldan 488 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → 𝑦 ⊆ dom 𝐹)
38 funimass3 6496 . . . . . . . . . . . 12 ((Fun 𝐹𝑦 ⊆ dom 𝐹) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
3925, 37, 38syl2anc 696 . . . . . . . . . . 11 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
4039biimpd 219 . . . . . . . . . 10 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
4140impr 650 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝑦 ⊆ (𝐹𝐴))
42 filss 21858 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑦𝐿 ∧ (𝐹𝐴) ⊆ 𝑌𝑦 ⊆ (𝐹𝐴))) → (𝐹𝐴) ∈ 𝐿)
4315, 16, 23, 41, 42syl13anc 1479 . . . . . . . 8 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → (𝐹𝐴) ∈ 𝐿)
44 foimacnv 6315 . . . . . . . . . . 11 ((𝐹:𝑌onto𝑋𝐴𝑋) → (𝐹 “ (𝐹𝐴)) = 𝐴)
4544eqcomd 2766 . . . . . . . . . 10 ((𝐹:𝑌onto𝑋𝐴𝑋) → 𝐴 = (𝐹 “ (𝐹𝐴)))
46453ad2antl3 1203 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → 𝐴 = (𝐹 “ (𝐹𝐴)))
4746adantr 472 . . . . . . . 8 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝐴 = (𝐹 “ (𝐹𝐴)))
48 imaeq2 5620 . . . . . . . . . 10 (𝑥 = (𝐹𝐴) → (𝐹𝑥) = (𝐹 “ (𝐹𝐴)))
4948eqeq2d 2770 . . . . . . . . 9 (𝑥 = (𝐹𝐴) → (𝐴 = (𝐹𝑥) ↔ 𝐴 = (𝐹 “ (𝐹𝐴))))
5049rspcev 3449 . . . . . . . 8 (((𝐹𝐴) ∈ 𝐿𝐴 = (𝐹 “ (𝐹𝐴))) → ∃𝑥𝐿 𝐴 = (𝐹𝑥))
5143, 47, 50syl2anc 696 . . . . . . 7 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → ∃𝑥𝐿 𝐴 = (𝐹𝑥))
5251rexlimdvaa 3170 . . . . . 6 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴 → ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
5352expimpd 630 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ((𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴) → ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
54 simprr 813 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → 𝐴 = (𝐹𝑥))
55 imassrn 5635 . . . . . . . . 9 (𝐹𝑥) ⊆ ran 𝐹
56 forn 6279 . . . . . . . . . . 11 (𝐹:𝑌onto𝑋 → ran 𝐹 = 𝑋)
57563ad2ant3 1130 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ran 𝐹 = 𝑋)
5857adantr 472 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → ran 𝐹 = 𝑋)
5955, 58syl5sseq 3794 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → (𝐹𝑥) ⊆ 𝑋)
6054, 59eqsstrd 3780 . . . . . . 7 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → 𝐴𝑋)
61 eqimss2 3799 . . . . . . . . 9 (𝐴 = (𝐹𝑥) → (𝐹𝑥) ⊆ 𝐴)
62 imaeq2 5620 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
6362sseq1d 3773 . . . . . . . . . 10 (𝑦 = 𝑥 → ((𝐹𝑦) ⊆ 𝐴 ↔ (𝐹𝑥) ⊆ 𝐴))
6463rspcev 3449 . . . . . . . . 9 ((𝑥𝐿 ∧ (𝐹𝑥) ⊆ 𝐴) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6561, 64sylan2 492 . . . . . . . 8 ((𝑥𝐿𝐴 = (𝐹𝑥)) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6665adantl 473 . . . . . . 7 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6760, 66jca 555 . . . . . 6 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴))
6867rexlimdvaa 3170 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (∃𝑥𝐿 𝐴 = (𝐹𝑥) → (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
6953, 68impbid 202 . . . 4 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ((𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
7011, 69bitrd 268 . . 3 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
71703coml 1122 . 2 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋𝑋 ∈ V) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
727, 71mpd3an3 1574 1 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wrex 3051  Vcvv 3340  wss 3715  ccnv 5265  dom cdm 5266  ran crn 5267  cima 5269  Fun wfun 6043   Fn wfn 6044  wf 6045  ontowfo 6047  cfv 6049  (class class class)co 6813  fBascfbas 19936  filGencfg 19937  Filcfil 21850   FilMap cfm 21938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-fbas 19945  df-fg 19946  df-fil 21851  df-fm 21943
This theorem is referenced by:  fmid  21965
  Copyright terms: Public domain W3C validator