Theorem uspgrupgr 29123

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 2729	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2729	. . . . 5 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	isuspgr 29097	. . . 4 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
4		f1f 6720	. . . 4 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
5	3, 4	biimtrdi 253	. . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
6	1, 2	isupgr 29029	. . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ UPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
7	5, 6	sylibrd 259	. 2 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph))
8	7	pm2.43i 52	1 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3394   ∖ cdif 3900  ∅c0 4284  𝒫 cpw 4551  {csn 4577   class class class wbr 5092  dom cdm 5619  ⟶wf 6478  –1-1→wf1 6479  ‘cfv 6482   ≤ cle 11150  2c2 12183  ♯chash 14237  Vtxcvtx 28941  iEdgciedg 28942  UPGraphcupgr 29025  USPGraphcuspgr 29093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fv 6490  df-upgr 29027  df-uspgr 29095

This theorem is referenced by:  uspgrupgrushgr  29124  uspgruhgr  29129  usgrupgr  29130  uspgrun  29133  uspgrunop  29134  uspgredg2vtxeu  29165  1loopgrnb0  29448  uspgr2wlkeq  29591  uspgrn2crct  29753  wlkiswwlks2  29820  wlkiswwlks  29821  wlklnwwlkn  29829  clwlkclwwlk  29946  wlk2v2e  30101  isuspgrim0  47888  isuspgrimlem  47889  upgrimwlklem5  47895  upgrimwlk  47896  grlimprclnbgr  47990  grlimprclnbgrvtx  47993  grlimgredgex  47994  uspgropssxp  48138  uspgrsprf  48140