![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oen3g | Structured version Visualization version GIF version |
Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8383 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) |
Ref | Expression |
---|---|
f1oen3g | ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oeq1 6479 | . . . 4 ⊢ (𝑓 = 𝐹 → (𝑓:𝐴–1-1-onto→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | |
2 | 1 | spcegv 3542 | . . 3 ⊢ (𝐹 ∈ 𝑉 → (𝐹:𝐴–1-1-onto→𝐵 → ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) |
3 | 2 | imp 407 | . 2 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
4 | bren 8373 | . 2 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) | |
5 | 3, 4 | sylibr 235 | 1 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1765 ∈ wcel 2083 class class class wbr 4968 –1-1-onto→wf1o 6231 ≈ cen 8361 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-opab 5031 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-en 8365 |
This theorem is referenced by: f1oen2g 8381 unen 8451 domdifsn 8454 domunsncan 8471 sbthlem10 8490 domssex 8532 phplem2 8551 sucdom2 8567 pssnn 8589 f1finf1o 8598 oien 8855 infdifsn 8973 fin4en1 9584 fin23lem21 9614 hashf1lem2 13666 odinf 18424 gsumval3lem2 18751 gsumval3 18752 hmphen2 22095 fnpreimac 30102 pibt2 34250 |
Copyright terms: Public domain | W3C validator |