Theorem uspgrupgr 29272

Description: A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)

Assertion

Ref	Expression
uspgrupgr	⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)

Proof of Theorem uspgrupgr

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2740	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2740	. . . . 5 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	isuspgr 29246	. . . 4 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
4		f1f 6730	. . . 4 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
5	3, 4	biimtrdi 254	. . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
6	1, 2	isupgr 29178	. . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ UPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
7	5, 6	sylibrd 260	. 2 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph))
8	7	pm2.43i 52	1 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)

Syntax hints:   → wi 4   ∈ wcel 2119  {crab 3392   ∖ cdif 3887  ∅c0 4268  𝒫 cpw 4536  {csn 4562   class class class wbr 5079  dom cdm 5625  ⟶wf 6488  –1-1→wf1 6489  ‘cfv 6492   ≤ cle 11178  2c2 12234  ♯chash 14290  Vtxcvtx 29090  iEdgciedg 29091  UPGraphcupgr 29174  USPGraphcuspgr 29242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fv 6500  df-upgr 29176  df-uspgr 29244

This theorem is referenced by:  uspgrupgrushgr  29273  uspgruhgr  29278  usgrupgr  29279  uspgrun  29282  uspgrunop  29283  uspgredg2vtxeu  29314  1loopgrnb0  29596  uspgr2wlkeq  29739  uspgrn2crct  29901  wlkiswwlks2  29968  wlkiswwlks  29969  wlklnwwlkn  29977  clwlkclwwlk  30097  wlk2v2e  30252  isuspgrim0  48392  isuspgrimlem  48393  upgrimwlklem5  48399  upgrimwlk  48400  grlimprclnbgr  48494  grlimprclnbgrvtx  48497  grlimgredgex  48498  uspgropssxp  48642  uspgrsprf  48644