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 8825 as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024.) |
Ref | Expression |
---|---|
bren | ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | encv 8824 | . 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
2 | f1ofn 6780 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴) | |
3 | fndm 6600 | . . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴) | |
4 | vex 3447 | . . . . . . 7 ⊢ 𝑓 ∈ V | |
5 | 4 | dmex 7838 | . . . . . 6 ⊢ dom 𝑓 ∈ V |
6 | 3, 5 | eqeltrrdi 2847 | . . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V) |
7 | 2, 6 | syl 17 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V) |
8 | f1ofo 6786 | . . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) | |
9 | forn 6754 | . . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) | |
10 | 8, 9 | syl 17 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵) |
11 | 4 | rnex 7839 | . . . . 5 ⊢ ran 𝑓 ∈ V |
12 | 10, 11 | eqeltrrdi 2847 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V) |
13 | 7, 12 | jca 512 | . . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
14 | 13 | exlimiv 1933 | . 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
15 | breng 8825 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) | |
16 | 1, 14, 15 | pm5.21nii 379 | 1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 Vcvv 3443 class class class wbr 5103 dom cdm 5630 ran crn 5631 Fn wfn 6486 –onto→wfo 6489 –1-1-onto→wf1o 6490 ≈ cen 8813 |
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-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 ax-un 7662 |
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-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-xp 5636 df-rel 5637 df-cnv 5638 df-dm 5640 df-rn 5641 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-en 8817 |
This theorem is referenced by: domen 8834 f1oen3g 8839 ener 8874 en0OLD 8891 en0ALT 8892 ensn1OLD 8895 en1OLD 8899 en2snOLD 8919 unen 8923 enfixsn 8958 canth2 9007 mapen 9018 ssenen 9028 rexdif1enOLD 9036 dif1en 9037 dif1enOLD 9039 ssfiALT 9051 ensymfib 9064 entrfil 9065 phplem2 9085 php3 9089 phplem4OLD 9097 php3OLD 9101 isinf 9137 isinfOLD 9138 domunfican 9197 fiint 9201 mapfien2 9278 unxpwdom2 9457 isinffi 9861 infxpenc2 9891 fseqen 9896 dfac8b 9900 infpwfien 9931 dfac12r 10015 infmap2 10087 cff1 10127 infpssr 10177 fin4en1 10178 enfin2i 10190 enfin1ai 10253 axcc3 10307 axcclem 10326 numth 10341 ttukey2g 10385 canthnum 10518 canthwe 10520 canthp1 10523 pwfseq 10533 tskuni 10652 gruen 10681 hasheqf1o 14176 hashfacen 14278 hashfacenOLD 14279 fz1f1o 15529 ruc 16059 cnso 16063 eulerth 16589 ablfaclem3 19795 lbslcic 21170 uvcendim 21176 indishmph 23071 ufldom 23235 ovolctb 24776 ovoliunlem3 24790 iunmbl2 24843 dyadmbl 24886 vitali 24899 cusgrfilem3 28203 padct 31430 f1ocnt 31499 volmeas 32603 eulerpart 32755 derangenlem 33538 mblfinlem1 36010 sticksstones4 40452 sticksstones20 40469 eldioph2lem1 40948 isnumbasgrplem1 41293 nnf1oxpnn 43172 sprsymrelen 45441 prproropen 45449 uspgrspren 45803 uspgrbisymrel 45805 1aryenef 46480 2aryenef 46491 rrx2xpreen 46554 |
Copyright terms: Public domain | W3C validator |