![]() |
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.) |
Ref | Expression |
---|---|
bren | ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | encv 8117 | . 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
2 | f1ofn 6279 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴) | |
3 | fndm 6130 | . . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴) | |
4 | vex 3354 | . . . . . . 7 ⊢ 𝑓 ∈ V | |
5 | 4 | dmex 7246 | . . . . . 6 ⊢ dom 𝑓 ∈ V |
6 | 3, 5 | syl6eqelr 2859 | . . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V) |
7 | 2, 6 | syl 17 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V) |
8 | f1ofo 6285 | . . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) | |
9 | forn 6259 | . . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) | |
10 | 8, 9 | syl 17 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵) |
11 | 4 | rnex 7247 | . . . . 5 ⊢ ran 𝑓 ∈ V |
12 | 10, 11 | syl6eqelr 2859 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V) |
13 | 7, 12 | jca 501 | . . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
14 | 13 | exlimiv 2010 | . 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
15 | f1oeq2 6269 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝑦)) | |
16 | 15 | exbidv 2002 | . . 3 ⊢ (𝑥 = 𝐴 → (∃𝑓 𝑓:𝑥–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝑦)) |
17 | f1oeq3 6270 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝑓:𝐴–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝐵)) | |
18 | 17 | exbidv 2002 | . . 3 ⊢ (𝑦 = 𝐵 → (∃𝑓 𝑓:𝐴–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) |
19 | df-en 8110 | . . 3 ⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} | |
20 | 16, 18, 19 | brabg 5127 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) |
21 | 1, 14, 20 | pm5.21nii 367 | 1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 = wceq 1631 ∃wex 1852 ∈ wcel 2145 Vcvv 3351 class class class wbr 4786 dom cdm 5249 ran crn 5250 Fn wfn 6026 –onto→wfo 6029 –1-1-onto→wf1o 6030 ≈ cen 8106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pr 5034 ax-un 7096 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-xp 5255 df-rel 5256 df-cnv 5257 df-dm 5259 df-rn 5260 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-en 8110 |
This theorem is referenced by: domen 8122 f1oen3g 8125 ener 8156 en0 8172 ensn1 8173 en1 8176 unen 8196 enfixsn 8225 canth2 8269 mapen 8280 ssenen 8290 phplem4 8298 php3 8302 isinf 8329 ssfi 8336 domunfican 8389 fiint 8393 mapfien2 8470 unxpwdom2 8649 isinffi 9018 infxpenc2 9045 fseqen 9050 dfac8b 9054 infpwfien 9085 dfac12r 9170 infmap2 9242 cff1 9282 infpssr 9332 fin4en1 9333 enfin2i 9345 enfin1ai 9408 axcc3 9462 axcclem 9481 numth 9496 ttukey2g 9540 canthnum 9673 canthwe 9675 canthp1 9678 pwfseq 9688 tskuni 9807 gruen 9836 hasheqf1o 13341 hashfacen 13440 fz1f1o 14649 ruc 15178 cnso 15182 eulerth 15695 ablfaclem3 18694 lbslcic 20397 uvcendim 20403 indishmph 21822 ufldom 21986 ovolctb 23478 ovoliunlem3 23492 iunmbl2 23545 dyadmbl 23588 vitali 23601 cusgrfilem3 26588 padct 29837 f1ocnt 29899 volmeas 30634 eulerpart 30784 derangenlem 31491 mblfinlem1 33779 eldioph2lem1 37849 isnumbasgrplem1 38197 nnf1oxpnn 39904 sprsymrelen 42278 uspgrspren 42288 uspgrbisymrel 42290 |
Copyright terms: Public domain | W3C validator |