Theorem f1osng 5610

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.)

Assertion

Ref	Expression
f1osng	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})

Proof of Theorem f1osng

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sneq 3677	. . . 4 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
2		f1oeq2 5557	. . . 4 ⊢ ({𝑎} = {𝐴} → ({⟨𝑎, 𝑏⟩}:{𝑎}–1-1-onto→{𝑏} ↔ {⟨𝑎, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
3	1, 2	syl 14	. . 3 ⊢ (𝑎 = 𝐴 → ({⟨𝑎, 𝑏⟩}:{𝑎}–1-1-onto→{𝑏} ↔ {⟨𝑎, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
4		opeq1 3856	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
5	4	sneqd 3679	. . . 4 ⊢ (𝑎 = 𝐴 → {⟨𝑎, 𝑏⟩} = {⟨𝐴, 𝑏⟩})
6		f1oeq1 5556	. . . 4 ⊢ ({⟨𝑎, 𝑏⟩} = {⟨𝐴, 𝑏⟩} → ({⟨𝑎, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
7	5, 6	syl 14	. . 3 ⊢ (𝑎 = 𝐴 → ({⟨𝑎, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
8	3, 7	bitrd 188	. 2 ⊢ (𝑎 = 𝐴 → ({⟨𝑎, 𝑏⟩}:{𝑎}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
9		sneq 3677	. . . 4 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
10		f1oeq3 5558	. . . 4 ⊢ ({𝑏} = {𝐵} → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝐵}))
11	9, 10	syl 14	. . 3 ⊢ (𝑏 = 𝐵 → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝐵}))
12		opeq2 3857	. . . . 5 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
13	12	sneqd 3679	. . . 4 ⊢ (𝑏 = 𝐵 → {⟨𝐴, 𝑏⟩} = {⟨𝐴, 𝐵⟩})
14		f1oeq1 5556	. . . 4 ⊢ ({⟨𝐴, 𝑏⟩} = {⟨𝐴, 𝐵⟩} → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝐵} ↔ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}))
15	13, 14	syl 14	. . 3 ⊢ (𝑏 = 𝐵 → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝐵} ↔ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}))
16	11, 15	bitrd 188	. 2 ⊢ (𝑏 = 𝐵 → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}))
17		vex 2802	. . 3 ⊢ 𝑎 ∈ V
18		vex 2802	. . 3 ⊢ 𝑏 ∈ V
19	17, 18	f1osn 5609	. 2 ⊢ {⟨𝑎, 𝑏⟩}:{𝑎}–1-1-onto→{𝑏}
20	8, 16, 19	vtocl2g 2865	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {csn 3666  ⟨cop 3669  –1-1-onto→wf1o 5313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-opab 4145  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-rn 4727  df-fun 5316  df-fn 5317  df-f 5318  df-f1 5319  df-fo 5320  df-f1o 5321

This theorem is referenced by:  f1sng  5611  f1oprg  5613  fsnunf  5832  dif1en  7029  1fv  10323  zfz1isolem1  11049  sumsnf  11906  prodsnf  12089  ennnfonelemhf1o  12970