| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bren | Structured version Visualization version GIF version | ||
| Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8994 as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024.) |
| Ref | Expression |
|---|---|
| bren | ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | encv 8993 | . 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
| 2 | f1ofn 6849 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴) | |
| 3 | fndm 6671 | . . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴) | |
| 4 | vex 3484 | . . . . . . 7 ⊢ 𝑓 ∈ V | |
| 5 | 4 | dmex 7931 | . . . . . 6 ⊢ dom 𝑓 ∈ V |
| 6 | 3, 5 | eqeltrrdi 2850 | . . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V) |
| 7 | 2, 6 | syl 17 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V) |
| 8 | f1ofo 6855 | . . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) | |
| 9 | forn 6823 | . . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) | |
| 10 | 8, 9 | syl 17 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵) |
| 11 | 4 | rnex 7932 | . . . . 5 ⊢ ran 𝑓 ∈ V |
| 12 | 10, 11 | eqeltrrdi 2850 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V) |
| 13 | 7, 12 | jca 511 | . . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 14 | 13 | exlimiv 1930 | . 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 15 | breng 8994 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) | |
| 16 | 1, 14, 15 | pm5.21nii 378 | 1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 class class class wbr 5143 dom cdm 5685 ran crn 5686 Fn wfn 6556 –onto→wfo 6559 –1-1-onto→wf1o 6560 ≈ cen 8982 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-xp 5691 df-rel 5692 df-cnv 5693 df-dm 5695 df-rn 5696 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-en 8986 |
| This theorem is referenced by: domen 9002 f1oen3g 9007 ener 9041 en0ALT 9059 unen 9086 enfixsn 9121 canth2 9170 mapen 9181 ssenen 9191 rexdif1enOLD 9199 dif1en 9200 dif1enOLD 9202 ssfiALT 9214 ensymfib 9224 entrfil 9225 phplem2 9245 php3 9249 phplem4OLD 9257 php3OLD 9261 isinf 9296 isinfOLD 9297 domunfican 9361 fiint 9366 fiintOLD 9367 mapfien2 9449 unxpwdom2 9628 isinffi 10032 infxpenc2 10062 fseqen 10067 dfac8b 10071 infpwfien 10102 dfac12r 10187 infmap2 10257 cff1 10298 infpssr 10348 fin4en1 10349 enfin2i 10361 enfin1ai 10424 axcc3 10478 axcclem 10497 numth 10512 ttukey2g 10556 canthnum 10689 canthwe 10691 canthp1 10694 pwfseq 10704 tskuni 10823 gruen 10852 hasheqf1o 14388 hashfacen 14493 fz1f1o 15746 ruc 16279 cnso 16283 eulerth 16820 ablfaclem3 20107 lbslcic 21861 uvcendim 21867 indishmph 23806 ufldom 23970 ovolctb 25525 ovoliunlem3 25539 iunmbl2 25592 dyadmbl 25635 vitali 25648 cusgrfilem3 29475 padct 32731 f1ocnt 32804 volmeas 34232 eulerpart 34384 derangenlem 35176 mblfinlem1 37664 sticksstones4 42150 sticksstones20 42167 eldioph2lem1 42771 isnumbasgrplem1 43113 nnf1oxpnn 45200 sprsymrelen 47487 prproropen 47495 uspgrspren 48068 uspgrbisymrel 48070 1aryenef 48566 2aryenef 48577 rrx2xpreen 48640 |
| Copyright terms: Public domain | W3C validator |