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 7849 | . 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
2 | f1ofn 6051 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴) | |
3 | fndm 5904 | . . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴) | |
4 | vex 3176 | . . . . . . 7 ⊢ 𝑓 ∈ V | |
5 | 4 | dmex 6991 | . . . . . 6 ⊢ dom 𝑓 ∈ V |
6 | 3, 5 | syl6eqelr 2697 | . . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V) |
7 | 2, 6 | syl 17 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V) |
8 | f1ofo 6057 | . . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) | |
9 | forn 6031 | . . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) | |
10 | 8, 9 | syl 17 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵) |
11 | 4 | rnex 6992 | . . . . 5 ⊢ ran 𝑓 ∈ V |
12 | 10, 11 | syl6eqelr 2697 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V) |
13 | 7, 12 | jca 553 | . . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
14 | 13 | exlimiv 1845 | . 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
15 | f1oeq2 6041 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝑦)) | |
16 | 15 | exbidv 1837 | . . 3 ⊢ (𝑥 = 𝐴 → (∃𝑓 𝑓:𝑥–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝑦)) |
17 | f1oeq3 6042 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝑓:𝐴–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝐵)) | |
18 | 17 | exbidv 1837 | . . 3 ⊢ (𝑦 = 𝐵 → (∃𝑓 𝑓:𝐴–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) |
19 | df-en 7842 | . . 3 ⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} | |
20 | 16, 18, 19 | brabg 4919 | . 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 195 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 class class class wbr 4583 dom cdm 5038 ran crn 5039 Fn wfn 5799 –onto→wfo 5802 –1-1-onto→wf1o 5803 ≈ cen 7838 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-xp 5044 df-rel 5045 df-cnv 5046 df-dm 5048 df-rn 5049 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-en 7842 |
This theorem is referenced by: domen 7854 f1oen3g 7857 ener 7888 enerOLD 7889 en0 7905 ensn1 7906 en1 7909 unen 7925 enfixsn 7954 canth2 7998 mapen 8009 ssenen 8019 phplem4 8027 php3 8031 isinf 8058 ssfi 8065 domunfican 8118 fiint 8122 mapfien2 8197 unxpwdom2 8376 isinffi 8701 infxpenc2 8728 fseqen 8733 dfac8b 8737 infpwfien 8768 dfac12r 8851 infmap2 8923 cff1 8963 infpssr 9013 fin4en1 9014 enfin2i 9026 enfin1ai 9089 axcc3 9143 axcclem 9162 numth 9177 ttukey2g 9221 canthnum 9350 canthwe 9352 canthp1 9355 pwfseq 9365 tskuni 9484 gruen 9513 hasheqf1o 12999 hashfacen 13095 fz1f1o 14288 ruc 14811 cnso 14815 eulerth 15326 ablfaclem3 18309 lbslcic 19999 uvcendim 20005 indishmph 21411 ufldom 21576 ovolctb 23065 ovoliunlem3 23079 iunmbl2 23132 dyadmbl 23174 vitali 23188 nbusgrafi 25977 cusgrafilem3 26009 wlknwwlknen 26243 padct 28885 f1ocnt 28946 volmeas 29621 eulerpart 29771 derangenlem 30407 mblfinlem1 32616 eldioph2lem1 36341 isnumbasgrplem1 36690 nnf1oxpnn 38379 cusgrfilem3 40673 wlknwwlksnen 41090 |
Copyright terms: Public domain | W3C validator |