![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1osn | Structured version Visualization version GIF version |
Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
f1osn.1 | ⊢ 𝐴 ∈ V |
f1osn.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
f1osn | ⊢ {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1osn.1 | . . 3 ⊢ 𝐴 ∈ V | |
2 | f1osn.2 | . . 3 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | fnsn 6556 | . 2 ⊢ {〈𝐴, 𝐵〉} Fn {𝐴} |
4 | 2, 1 | fnsn 6556 | . . 3 ⊢ {〈𝐵, 𝐴〉} Fn {𝐵} |
5 | 1, 2 | cnvsn 6176 | . . . 4 ⊢ ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉} |
6 | 5 | fneq1i 6596 | . . 3 ⊢ (◡{〈𝐴, 𝐵〉} Fn {𝐵} ↔ {〈𝐵, 𝐴〉} Fn {𝐵}) |
7 | 4, 6 | mpbir 230 | . 2 ⊢ ◡{〈𝐴, 𝐵〉} Fn {𝐵} |
8 | dff1o4 6789 | . 2 ⊢ ({〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵} ↔ ({〈𝐴, 𝐵〉} Fn {𝐴} ∧ ◡{〈𝐴, 𝐵〉} Fn {𝐵})) | |
9 | 3, 7, 8 | mpbir2an 709 | 1 ⊢ {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3443 {csn 4584 〈cop 4590 ◡ccnv 5630 Fn wfn 6488 –1-1-onto→wf1o 6492 |
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 |
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-mo 2539 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-br 5104 df-opab 5166 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 |
This theorem is referenced by: f1osng 6822 fsn 7077 ensn1 8919 ensn1OLD 8920 pssnn 9070 phplem2OLD 9120 isinf 9162 isinfOLD 9163 pssnnOLD 9167 ac6sfi 9189 marypha1lem 9327 hashf1lem1 14306 hashf1lem1OLD 14307 0ram 16851 mdet0f1o 21893 imasdsf1olem 23677 istrkg2ld 27230 axlowdimlem10 27728 subfacp1lem5 33581 poimirlem3 36012 grposnOLD 36272 |
Copyright terms: Public domain | W3C validator |