Theorem fo1st 4082

Description: The 1^st function maps the universe onto the universe.

Assertion

Ref	Expression
fo1st	⊢ 1st :V–onto→V

Proof of Theorem fo1st

Step	Hyp	Ref	Expression
1		df-fo 3191	. . 3 ⊢ ({⟨x, y⟩∣y = ∪dom { x}}:V–onto→V ↔ ({⟨x, y⟩∣y = ∪dom { x}} Fn V ⋀ ran {⟨x, y⟩∣y = ∪dom { x}} = V))
2		snex 2745	. . . . . 6 ⊢ {x} ∈ V
3	2	dmex 3354	. . . . 5 ⊢ dom { x} ∈ V
4	3	uniex 2865	. . . 4 ⊢ ∪dom { x} ∈ V
5		visset 1809	. . . . . 6 ⊢ x ∈ V
6	5	biantrur 724	. . . . 5 ⊢ (y = ∪dom { x} ↔ (x ∈ V ⋀ y = ∪dom { x}))
7	6	opabbii 2666	. . . 4 ⊢ {⟨x, y⟩∣y = ∪dom { x}} = {⟨x, y⟩∣(x ∈ V ⋀ y = ∪dom { x})}
8	4, 7	fnopab2 3611	. . 3 ⊢ {⟨x, y⟩∣y = ∪dom { x}} Fn V
9		visset 1809	. . . . . . . . 9 ⊢ y ∈ V
10	9	op1sta 3441	. . . . . . . 8 ⊢ ∪dom {⟨y, y⟩} = y
11	10	eqcomi 1476	. . . . . . 7 ⊢ y = ∪dom {⟨y, y⟩}
12		opex 2777	. . . . . . . 8 ⊢ ⟨y, y⟩ ∈ V
13		sneq 2413	. . . . . . . . . . 11 ⊢ (x = ⟨y, y⟩ → {x} = {⟨y, y⟩})
14	13	dmeqd 3308	. . . . . . . . . 10 ⊢ (x = ⟨y, y⟩ → dom { x} = dom {⟨y, y⟩})
15	14	unieqd 2507	. . . . . . . . 9 ⊢ (x = ⟨y, y⟩ → ∪dom { x} = ∪dom {⟨y, y⟩})
16	15	eqeq2d 1483	. . . . . . . 8 ⊢ (x = ⟨y, y⟩ → (y = ∪dom { x} ↔ y = ∪dom {⟨y, y⟩}))
17	12, 16	cla4ev 1865	. . . . . . 7 ⊢ (y = ∪dom {⟨y, y⟩} → ∃x y = ∪dom { x})
18	11, 17	ax-mp 7	. . . . . 6 ⊢ ∃x y = ∪dom { x}
19		equid 1124	. . . . . 6 ⊢ y = y
20	18, 19	2th 717	. . . . 5 ⊢ (∃x y = ∪dom { x} ↔ y = y)
21	20	abbii 1572	. . . 4 ⊢ {y∣∃x y = ∪dom { x}} = {y∣y = y}
22		rnopab 3347	. . . 4 ⊢ ran {⟨x, y⟩∣y = ∪dom { x}} = {y∣∃x y = ∪dom { x}}
23		df-v 1808	. . . 4 ⊢ V = {y∣y = y}
24	21, 22, 23	3eqtr4 1502	. . 3 ⊢ ran {⟨x, y⟩∣y = ∪dom { x}} = V
25	1, 8, 24	mpbir2an 729	. 2 ⊢ {⟨x, y⟩∣y = ∪dom { x}}:V–onto→V
26		df-1st 4070	. . 3 ⊢ 1st = {⟨x, y⟩∣y = ∪dom { x}}
27		foeq1 3660	. . 3 ⊢ (1st = {⟨x, y⟩∣y = ∪dom { x}} → (1st :V–onto→V ↔ {⟨x, y⟩∣y = ∪dom { x}}:V–onto→V))
28	26, 27	ax-mp 7	. 2 ⊢ (1st :V–onto→V ↔ {⟨x, y⟩∣y = ∪dom { x}}:V–onto→V)
29	25, 28	mpbir 190	1 ⊢ 1st :V–onto→V

Syntax hints:   ↔ wb 146   ⋀ wa 223   = wceq 954   ∈ wcel 956  ∃wex 978  {cab 1461  Vcvv 1807  {csn 2405  ⟨cop 2407  ∪cuni 2498  {copab 2661  dom cdm 3165  ran crn 3166   Fn wfn 3172  –onto→wfo 3175  1^st c1st 4068

This theorem is referenced by:  1stcof 4092  df1st2 4117  ruclem10 7471  bcthlem3 7952  vafval 8175  smfval 8177  0vfval 8178  vsfval 8207  domval 10537  codval 10538  idval 10539

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-id 2830  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-fun 3187  df-fn 3188  df-fo 3191  df-1st 4070

Copyright terms: Public domain