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

Theorem elfm3 21659
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 6079 . . . 4 (𝐹:𝑌onto𝑋 → (𝐹𝑌) = 𝑋)
21adantl 482 . . 3 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝑌) = 𝑋)
3 fofun 6075 . . . 4 (𝐹:𝑌onto𝑋 → Fun 𝐹)
4 elfvdm 6178 . . . 4 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
5 funimaexg 5935 . . . 4 ((Fun 𝐹𝑌 ∈ dom fBas) → (𝐹𝑌) ∈ V)
63, 4, 5syl2anr 495 . . 3 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝑌) ∈ V)
72, 6eqeltrrd 2705 . 2 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → 𝑋 ∈ V)
8 fof 6074 . . . . 5 (𝐹:𝑌onto𝑋𝐹:𝑌𝑋)
9 elfm2.l . . . . . 6 𝐿 = (𝑌filGen𝐵)
109elfm2 21657 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
118, 10syl3an3 1358 . . . 4 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
12 fgcl 21587 . . . . . . . . . . . 12 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
139, 12syl5eqel 2708 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → 𝐿 ∈ (Fil‘𝑌))
14133ad2ant2 1081 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → 𝐿 ∈ (Fil‘𝑌))
1514ad2antrr 761 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝐿 ∈ (Fil‘𝑌))
16 simprl 793 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝑦𝐿)
17 cnvimass 5448 . . . . . . . . . . . 12 (𝐹𝐴) ⊆ dom 𝐹
18 fofn 6076 . . . . . . . . . . . . 13 (𝐹:𝑌onto𝑋𝐹 Fn 𝑌)
19 fndm 5950 . . . . . . . . . . . . 13 (𝐹 Fn 𝑌 → dom 𝐹 = 𝑌)
2018, 19syl 17 . . . . . . . . . . . 12 (𝐹:𝑌onto𝑋 → dom 𝐹 = 𝑌)
2117, 20syl5sseq 3637 . . . . . . . . . . 11 (𝐹:𝑌onto𝑋 → (𝐹𝐴) ⊆ 𝑌)
22213ad2ant3 1082 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝐴) ⊆ 𝑌)
2322ad2antrr 761 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → (𝐹𝐴) ⊆ 𝑌)
2433ad2ant3 1082 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → Fun 𝐹)
2524ad2antrr 761 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → Fun 𝐹)
269eleq2i 2696 . . . . . . . . . . . . . . 15 (𝑦𝐿𝑦 ∈ (𝑌filGen𝐵))
27 elfg 21580 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (fBas‘𝑌) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
28273ad2ant2 1081 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
2928adantr 481 . . . . . . . . . . . . . . 15 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
3026, 29syl5bb 272 . . . . . . . . . . . . . 14 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (𝑦𝐿 ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
3130simprbda 652 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → 𝑦𝑌)
32 sseq2 3611 . . . . . . . . . . . . . . . . 17 (dom 𝐹 = 𝑌 → (𝑦 ⊆ dom 𝐹𝑦𝑌))
3332biimpar 502 . . . . . . . . . . . . . . . 16 ((dom 𝐹 = 𝑌𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3420, 33sylan 488 . . . . . . . . . . . . . . 15 ((𝐹:𝑌onto𝑋𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
35343ad2antl3 1223 . . . . . . . . . . . . . 14 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3635adantlr 750 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3731, 36syldan 487 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → 𝑦 ⊆ dom 𝐹)
38 funimass3 6290 . . . . . . . . . . . 12 ((Fun 𝐹𝑦 ⊆ dom 𝐹) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
3925, 37, 38syl2anc 692 . . . . . . . . . . 11 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
4039biimpd 219 . . . . . . . . . 10 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
4140impr 648 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝑦 ⊆ (𝐹𝐴))
42 filss 21562 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑦𝐿 ∧ (𝐹𝐴) ⊆ 𝑌𝑦 ⊆ (𝐹𝐴))) → (𝐹𝐴) ∈ 𝐿)
4315, 16, 23, 41, 42syl13anc 1325 . . . . . . . 8 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → (𝐹𝐴) ∈ 𝐿)
44 foimacnv 6113 . . . . . . . . . . 11 ((𝐹:𝑌onto𝑋𝐴𝑋) → (𝐹 “ (𝐹𝐴)) = 𝐴)
4544eqcomd 2632 . . . . . . . . . 10 ((𝐹:𝑌onto𝑋𝐴𝑋) → 𝐴 = (𝐹 “ (𝐹𝐴)))
46453ad2antl3 1223 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → 𝐴 = (𝐹 “ (𝐹𝐴)))
4746adantr 481 . . . . . . . 8 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝐴 = (𝐹 “ (𝐹𝐴)))
48 imaeq2 5425 . . . . . . . . . 10 (𝑥 = (𝐹𝐴) → (𝐹𝑥) = (𝐹 “ (𝐹𝐴)))
4948eqeq2d 2636 . . . . . . . . 9 (𝑥 = (𝐹𝐴) → (𝐴 = (𝐹𝑥) ↔ 𝐴 = (𝐹 “ (𝐹𝐴))))
5049rspcev 3300 . . . . . . . 8 (((𝐹𝐴) ∈ 𝐿𝐴 = (𝐹 “ (𝐹𝐴))) → ∃𝑥𝐿 𝐴 = (𝐹𝑥))
5143, 47, 50syl2anc 692 . . . . . . 7 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → ∃𝑥𝐿 𝐴 = (𝐹𝑥))
5251rexlimdvaa 3030 . . . . . 6 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴 → ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
5352expimpd 628 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ((𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴) → ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
54 simprr 795 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → 𝐴 = (𝐹𝑥))
55 imassrn 5440 . . . . . . . . 9 (𝐹𝑥) ⊆ ran 𝐹
56 forn 6077 . . . . . . . . . . 11 (𝐹:𝑌onto𝑋 → ran 𝐹 = 𝑋)
57563ad2ant3 1082 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ran 𝐹 = 𝑋)
5857adantr 481 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → ran 𝐹 = 𝑋)
5955, 58syl5sseq 3637 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → (𝐹𝑥) ⊆ 𝑋)
6054, 59eqsstrd 3623 . . . . . . 7 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → 𝐴𝑋)
61 eqimss2 3642 . . . . . . . . 9 (𝐴 = (𝐹𝑥) → (𝐹𝑥) ⊆ 𝐴)
62 imaeq2 5425 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
6362sseq1d 3616 . . . . . . . . . 10 (𝑦 = 𝑥 → ((𝐹𝑦) ⊆ 𝐴 ↔ (𝐹𝑥) ⊆ 𝐴))
6463rspcev 3300 . . . . . . . . 9 ((𝑥𝐿 ∧ (𝐹𝑥) ⊆ 𝐴) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6561, 64sylan2 491 . . . . . . . 8 ((𝑥𝐿𝐴 = (𝐹𝑥)) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6665adantl 482 . . . . . . 7 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6760, 66jca 554 . . . . . 6 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴))
6867rexlimdvaa 3030 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (∃𝑥𝐿 𝐴 = (𝐹𝑥) → (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
6953, 68impbid 202 . . . 4 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ((𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
7011, 69bitrd 268 . . 3 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
71703coml 1269 . 2 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋𝑋 ∈ V) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
727, 71mpd3an3 1422 1 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1992  wrex 2913  Vcvv 3191  wss 3560  ccnv 5078  dom cdm 5079  ran crn 5080  cima 5082  Fun wfun 5844   Fn wfn 5845  wf 5846  ontowfo 5848  cfv 5850  (class class class)co 6605  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-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-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  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-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-fbas 19657  df-fg 19658  df-fil 21555  df-fm 21647
This theorem is referenced by:  fmid  21669
  Copyright terms: Public domain W3C validator