Theorem uspgrf1oedg 29309

Description: The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)

Hypothesis

Ref	Expression
usgrf1o.e	⊢ 𝐸 = (iEdg‘𝐺)

Assertion

Ref	Expression
uspgrf1oedg	⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))

Proof of Theorem uspgrf1oedg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2752	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		usgrf1o.e	. . 3 ⊢ 𝐸 = (iEdg‘𝐺)
3	1, 2	uspgrf 29290	. 2 ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
4		f1f1orn 6803	. . 3 ⊢ (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
5	2	rneqi 5902	. . . . 5 ⊢ ran 𝐸 = ran (iEdg‘𝐺)
6		edgval 29185	. . . . 5 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
7	5, 6	eqtr4i 2778	. . . 4 ⊢ ran 𝐸 = (Edg‘𝐺)
8		f1oeq3 6781	. . . 4 ⊢ (ran 𝐸 = (Edg‘𝐺) → (𝐸:dom 𝐸–1-1-onto→ran 𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)))
9	7, 8	ax-mp 5	. . 3 ⊢ (𝐸:dom 𝐸–1-1-onto→ran 𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))
10	4, 9	sylib 220	. 2 ⊢ (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))
11	3, 10	syl 17	1 ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550   ∈ wcel 2132  {crab 3404   ∖ cdif 3892  ∅c0 4276  𝒫 cpw 4545  {csn 4572   class class class wbr 5090  dom cdm 5636  ran crn 5637  –1-1→wf1 6503  –1-1-onto→wf1o 6505  ‘cfv 6506   ≤ cle 11203  2c2 12258  ♯chash 14329  Vtxcvtx 29132  iEdgciedg 29133  Edgcedg 29183  USPGraphcuspgr 29284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-edg 29184  df-uspgr 29286

This theorem is referenced by:  uspgredgiedg  29311  uspgriedgedg  29312  uspgr2wlkeq  29781  wlkiswwlks2lem4  30007  wlkiswwlks2lem5  30008  clwlkclwwlk  30139  isuspgrim0lem  48453  upgrimwlklem2  48458  upgrimwlklem3  48459  upgrimtrlslem2  48465  upgrimtrls  48466  uspgrlimlem1  48548  uspgrlimlem2  48549  uspgrlimlem3  48550  uspgrlimlem4  48551  uspgrlim  48552