![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffo3 | Structured version Visualization version GIF version |
Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.) |
Ref | Expression |
---|---|
dffo3 | ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dffo2 6761 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) | |
2 | ffn 6669 | . . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | fnrnfv 6903 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) | |
4 | 3 | eqeq1d 2735 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
5 | 2, 4 | syl 17 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
6 | dfbi2 476 | . . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) | |
7 | simpr 486 | . . . . . . . . . 10 ⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 = (𝐹‘𝑥)) | |
8 | ffvelcdm 7033 | . . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | |
9 | 8 | adantr 482 | . . . . . . . . . 10 ⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵) |
10 | 7, 9 | eqeltrd 2834 | . . . . . . . . 9 ⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 ∈ 𝐵) |
11 | 10 | rexlimdva2 3151 | . . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)) |
12 | 11 | biantrurd 534 | . . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → ((𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))))) |
13 | 6, 12 | bitr4id 290 | . . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
14 | 13 | albidv 1924 | . . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
15 | eqabc 2876 | . . . . 5 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵)) | |
16 | df-ral 3062 | . . . . 5 ⊢ (∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | |
17 | 14, 15, 16 | 3bitr4g 314 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
18 | 5, 17 | bitrd 279 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
19 | 18 | pm5.32i 576 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
20 | 1, 19 | bitri 275 | 1 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 = wceq 1542 ∈ wcel 2107 {cab 2710 ∀wral 3061 ∃wrex 3070 ran crn 5635 Fn wfn 6492 ⟶wf 6493 –onto→wfo 6495 ‘cfv 6497 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-fo 6503 df-fv 6505 |
This theorem is referenced by: dffo4 7054 foelrn 7057 foco2 7058 fcofo 7235 foov 7529 fsetfocdm 8802 resixpfo 8877 fofinf1o 9274 wdom2d 9521 brwdom3 9523 isf32lem9 10302 hsmexlem2 10368 cnref1o 12915 wwlktovfo 14853 1arith 16804 fullestrcsetc 18044 fullsetcestrc 18059 orbsta 19098 symgextfo 19209 symgfixfo 19226 pwssplit1 20535 znf1o 20974 cygznlem3 20992 scmatfo 21895 m2cpmfo 22121 pm2mpfo 22179 recosf1o 25907 efif1olem4 25917 dvdsmulf1o 26559 scutfo 27255 addsfo 27315 negsfo 27370 wlkswwlksf1o 28866 wwlksnextsurj 28887 clwlkclwwlkfo 28995 clwwlkfo 29036 eucrctshift 29229 frgrncvvdeqlem9 29293 numclwwlk1lem2fo 29344 subfacp1lem3 33833 cvmfolem 33930 finixpnum 36109 sticksstones3 40602 wessf1ornlem 43491 projf1o 43505 sumnnodd 43957 dvnprodlem1 44273 fourierdlem54 44487 nnfoctbdjlem 44782 isomenndlem 44857 fsetsnfo 45373 cfsetsnfsetfo 45380 sprsymrelfo 45775 prproropf1o 45785 isomuspgrlem2d 46109 uspgrsprfo 46136 1arymaptfo 46815 2arymaptfo 46826 rrx2xpref1o 46890 |
Copyright terms: Public domain | W3C validator |