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

Theorem elfm3 23301
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 6761 . . . 4 (𝐹:𝑌onto𝑋 → (𝐹𝑌) = 𝑋)
21adantl 482 . . 3 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝑌) = 𝑋)
3 fofun 6757 . . . 4 (𝐹:𝑌onto𝑋 → Fun 𝐹)
4 elfvdm 6879 . . . 4 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
5 funimaexg 6587 . . . 4 ((Fun 𝐹𝑌 ∈ dom fBas) → (𝐹𝑌) ∈ V)
63, 4, 5syl2anr 597 . . 3 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝑌) ∈ V)
72, 6eqeltrrd 2839 . 2 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → 𝑋 ∈ V)
8 fof 6756 . . . . 5 (𝐹:𝑌onto𝑋𝐹:𝑌𝑋)
9 elfm2.l . . . . . 6 𝐿 = (𝑌filGen𝐵)
109elfm2 23299 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
118, 10syl3an3 1165 . . . 4 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
12 fgcl 23229 . . . . . . . . . . . 12 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
139, 12eqeltrid 2842 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → 𝐿 ∈ (Fil‘𝑌))
14133ad2ant2 1134 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → 𝐿 ∈ (Fil‘𝑌))
1514ad2antrr 724 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝐿 ∈ (Fil‘𝑌))
16 simprl 769 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝑦𝐿)
17 cnvimass 6033 . . . . . . . . . . . 12 (𝐹𝐴) ⊆ dom 𝐹
18 fofn 6758 . . . . . . . . . . . . 13 (𝐹:𝑌onto𝑋𝐹 Fn 𝑌)
1918fndmd 6607 . . . . . . . . . . . 12 (𝐹:𝑌onto𝑋 → dom 𝐹 = 𝑌)
2017, 19sseqtrid 3996 . . . . . . . . . . 11 (𝐹:𝑌onto𝑋 → (𝐹𝐴) ⊆ 𝑌)
21203ad2ant3 1135 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐹𝐴) ⊆ 𝑌)
2221ad2antrr 724 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → (𝐹𝐴) ⊆ 𝑌)
2333ad2ant3 1135 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → Fun 𝐹)
2423ad2antrr 724 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → Fun 𝐹)
259eleq2i 2829 . . . . . . . . . . . . . . 15 (𝑦𝐿𝑦 ∈ (𝑌filGen𝐵))
26 elfg 23222 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (fBas‘𝑌) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
27263ad2ant2 1134 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
2827adantr 481 . . . . . . . . . . . . . . 15 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (𝑦 ∈ (𝑌filGen𝐵) ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
2925, 28bitrid 282 . . . . . . . . . . . . . 14 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (𝑦𝐿 ↔ (𝑦𝑌 ∧ ∃𝑧𝐵 𝑧𝑦)))
3029simprbda 499 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → 𝑦𝑌)
31 sseq2 3970 . . . . . . . . . . . . . . . . 17 (dom 𝐹 = 𝑌 → (𝑦 ⊆ dom 𝐹𝑦𝑌))
3231biimpar 478 . . . . . . . . . . . . . . . 16 ((dom 𝐹 = 𝑌𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3319, 32sylan 580 . . . . . . . . . . . . . . 15 ((𝐹:𝑌onto𝑋𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
34333ad2antl3 1187 . . . . . . . . . . . . . 14 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3534adantlr 713 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑌) → 𝑦 ⊆ dom 𝐹)
3630, 35syldan 591 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → 𝑦 ⊆ dom 𝐹)
37 funimass3 7004 . . . . . . . . . . . 12 ((Fun 𝐹𝑦 ⊆ dom 𝐹) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
3824, 36, 37syl2anc 584 . . . . . . . . . . 11 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
3938biimpd 228 . . . . . . . . . 10 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝐿) → ((𝐹𝑦) ⊆ 𝐴𝑦 ⊆ (𝐹𝐴)))
4039impr 455 . . . . . . . . 9 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝑦 ⊆ (𝐹𝐴))
41 filss 23204 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑦𝐿 ∧ (𝐹𝐴) ⊆ 𝑌𝑦 ⊆ (𝐹𝐴))) → (𝐹𝐴) ∈ 𝐿)
4215, 16, 22, 40, 41syl13anc 1372 . . . . . . . 8 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → (𝐹𝐴) ∈ 𝐿)
43 foimacnv 6801 . . . . . . . . . . 11 ((𝐹:𝑌onto𝑋𝐴𝑋) → (𝐹 “ (𝐹𝐴)) = 𝐴)
4443eqcomd 2742 . . . . . . . . . 10 ((𝐹:𝑌onto𝑋𝐴𝑋) → 𝐴 = (𝐹 “ (𝐹𝐴)))
45443ad2antl3 1187 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → 𝐴 = (𝐹 “ (𝐹𝐴)))
4645adantr 481 . . . . . . . 8 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → 𝐴 = (𝐹 “ (𝐹𝐴)))
47 imaeq2 6009 . . . . . . . . 9 (𝑥 = (𝐹𝐴) → (𝐹𝑥) = (𝐹 “ (𝐹𝐴)))
4847rspceeqv 3595 . . . . . . . 8 (((𝐹𝐴) ∈ 𝐿𝐴 = (𝐹 “ (𝐹𝐴))) → ∃𝑥𝐿 𝐴 = (𝐹𝑥))
4942, 46, 48syl2anc 584 . . . . . . 7 ((((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) ∧ (𝑦𝐿 ∧ (𝐹𝑦) ⊆ 𝐴)) → ∃𝑥𝐿 𝐴 = (𝐹𝑥))
5049rexlimdvaa 3153 . . . . . 6 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ 𝐴𝑋) → (∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴 → ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
5150expimpd 454 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ((𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴) → ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
52 simprr 771 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → 𝐴 = (𝐹𝑥))
53 imassrn 6024 . . . . . . . . 9 (𝐹𝑥) ⊆ ran 𝐹
54 forn 6759 . . . . . . . . . . 11 (𝐹:𝑌onto𝑋 → ran 𝐹 = 𝑋)
55543ad2ant3 1135 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ran 𝐹 = 𝑋)
5655adantr 481 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → ran 𝐹 = 𝑋)
5753, 56sseqtrid 3996 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → (𝐹𝑥) ⊆ 𝑋)
5852, 57eqsstrd 3982 . . . . . . 7 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → 𝐴𝑋)
59 eqimss2 4001 . . . . . . . . 9 (𝐴 = (𝐹𝑥) → (𝐹𝑥) ⊆ 𝐴)
60 imaeq2 6009 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
6160sseq1d 3975 . . . . . . . . . 10 (𝑦 = 𝑥 → ((𝐹𝑦) ⊆ 𝐴 ↔ (𝐹𝑥) ⊆ 𝐴))
6261rspcev 3581 . . . . . . . . 9 ((𝑥𝐿 ∧ (𝐹𝑥) ⊆ 𝐴) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6359, 62sylan2 593 . . . . . . . 8 ((𝑥𝐿𝐴 = (𝐹𝑥)) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6463adantl 482 . . . . . . 7 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)
6558, 64jca 512 . . . . . 6 (((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) ∧ (𝑥𝐿𝐴 = (𝐹𝑥))) → (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴))
6665rexlimdvaa 3153 . . . . 5 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (∃𝑥𝐿 𝐴 = (𝐹𝑥) → (𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴)))
6751, 66impbid 211 . . . 4 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → ((𝐴𝑋 ∧ ∃𝑦𝐿 (𝐹𝑦) ⊆ 𝐴) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
6811, 67bitrd 278 . . 3 ((𝑋 ∈ V ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
69683coml 1127 . 2 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋𝑋 ∈ V) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
707, 69mpd3an3 1462 1 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌onto𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥𝐿 𝐴 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wrex 3073  Vcvv 3445  wss 3910  ccnv 5632  dom cdm 5633  ran crn 5634  cima 5636  Fun wfun 6490  wf 6492  ontowfo 6494  cfv 6496  (class class class)co 7357  fBascfbas 20784  filGencfg 20785  Filcfil 23196   FilMap cfm 23284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-fbas 20793  df-fg 20794  df-fil 23197  df-fm 23289
This theorem is referenced by:  fmid  23311
  Copyright terms: Public domain W3C validator