Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1osng | Structured version Visualization version GIF version |
Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.) |
Ref | Expression |
---|---|
f1osng | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneq 4135 | . . . 4 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴}) | |
2 | f1oeq2 6041 | . . . 4 ⊢ ({𝑎} = {𝐴} → ({〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} ↔ {〈𝑎, 𝑏〉}:{𝐴}–1-1-onto→{𝑏})) | |
3 | 1, 2 | syl 17 | . . 3 ⊢ (𝑎 = 𝐴 → ({〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} ↔ {〈𝑎, 𝑏〉}:{𝐴}–1-1-onto→{𝑏})) |
4 | opeq1 4340 | . . . . 5 ⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) | |
5 | 4 | sneqd 4137 | . . . 4 ⊢ (𝑎 = 𝐴 → {〈𝑎, 𝑏〉} = {〈𝐴, 𝑏〉}) |
6 | f1oeq1 6040 | . . . 4 ⊢ ({〈𝑎, 𝑏〉} = {〈𝐴, 𝑏〉} → ({〈𝑎, 𝑏〉}:{𝐴}–1-1-onto→{𝑏} ↔ {〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝑏})) | |
7 | 5, 6 | syl 17 | . . 3 ⊢ (𝑎 = 𝐴 → ({〈𝑎, 𝑏〉}:{𝐴}–1-1-onto→{𝑏} ↔ {〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝑏})) |
8 | 3, 7 | bitrd 267 | . 2 ⊢ (𝑎 = 𝐴 → ({〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} ↔ {〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝑏})) |
9 | sneq 4135 | . . . 4 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵}) | |
10 | f1oeq3 6042 | . . . 4 ⊢ ({𝑏} = {𝐵} → ({〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝑏} ↔ {〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝐵})) | |
11 | 9, 10 | syl 17 | . . 3 ⊢ (𝑏 = 𝐵 → ({〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝑏} ↔ {〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝐵})) |
12 | opeq2 4341 | . . . . 5 ⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) | |
13 | 12 | sneqd 4137 | . . . 4 ⊢ (𝑏 = 𝐵 → {〈𝐴, 𝑏〉} = {〈𝐴, 𝐵〉}) |
14 | f1oeq1 6040 | . . . 4 ⊢ ({〈𝐴, 𝑏〉} = {〈𝐴, 𝐵〉} → ({〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝐵} ↔ {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵})) | |
15 | 13, 14 | syl 17 | . . 3 ⊢ (𝑏 = 𝐵 → ({〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝐵} ↔ {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵})) |
16 | 11, 15 | bitrd 267 | . 2 ⊢ (𝑏 = 𝐵 → ({〈𝐴, 𝑏〉}:{𝐴}–1-1-onto→{𝑏} ↔ {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵})) |
17 | vex 3176 | . . 3 ⊢ 𝑎 ∈ V | |
18 | vex 3176 | . . 3 ⊢ 𝑏 ∈ V | |
19 | 17, 18 | f1osn 6088 | . 2 ⊢ {〈𝑎, 𝑏〉}:{𝑎}–1-1-onto→{𝑏} |
20 | 8, 16, 19 | vtocl2g 3243 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 {csn 4125 〈cop 4131 –1-1-onto→wf1o 5803 |
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-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 |
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-br 4584 df-opab 4644 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 |
This theorem is referenced by: f1sng 6090 f1oprswap 6092 f1oprg 6093 f1o2sn 6314 fsnunf 6356 fsnex 6438 suppsnop 7196 ralxpmap 7793 enfixsn 7954 fseqenlem1 8730 canthp1lem2 9354 sumsn 14319 prodsn 14531 prodsnf 14533 vdwlem8 15530 gsumws1 17199 symg1bas 17639 dprdsn 18258 umgra1 25855 uslgra1 25901 usgra1 25902 vdgr1d 26430 vdgr1b 26431 vdgr1a 26433 eupa0 26501 eupap1 26503 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 mapfzcons 36297 sumsnd 38208 mapsnd 38383 sumsnf 38636 1hegrlfgr 40722 eupthp1 41384 |
Copyright terms: Public domain | W3C validator |