![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oen2g | Structured version Visualization version GIF version |
Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8324 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.) |
Ref | Expression |
---|---|
f1oen2g | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1of 6442 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | fex2 7452 | . . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) | |
3 | 1, 2 | syl3an1 1144 | . . 3 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) |
4 | 3 | 3coml 1108 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐹 ∈ V) |
5 | simp3 1119 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐹:𝐴–1-1-onto→𝐵) | |
6 | f1oen3g 8321 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | |
7 | 4, 5, 6 | syl2anc 576 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1069 ∈ wcel 2051 Vcvv 3410 class class class wbr 4926 ⟶wf 6182 –1-1-onto→wf1o 6185 ≈ cen 8302 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-en 8306 |
This theorem is referenced by: f1oeng 8324 enrefg 8337 en2d 8341 en3d 8342 ener 8352 f1imaen2g 8366 cnven 8381 xpcomen 8403 omxpen 8414 pw2eng 8418 unfilem3 8578 xpfi 8583 hsmexlem1 9645 iccen 12698 uzenom 13146 nnenom 13162 eqgen 18129 dfod2 18465 hmphen 22113 clwlkclwwlken 27542 clwlkclwwlkenOLD 27543 clwwlken 27590 clwwlkenOLD 27591 clwwlknonclwlknonen 27928 clwwlknonclwlknonenOLD 27929 dlwwlknondlwlknonen 27934 dlwwlknondlwlknonenOLD 27935 |
Copyright terms: Public domain | W3C validator |