Theorem uspgrupgr 29251

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 2736	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2736	. . . . 5 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	isuspgr 29225	. . . 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 253	. . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
6	1, 2	isupgr 29157	. . 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 2113  {crab 3399   ∖ cdif 3898  ∅c0 4285  𝒫 cpw 4554  {csn 4580   class class class wbr 5098  dom cdm 5624  ⟶wf 6488  –1-1→wf1 6489  ‘cfv 6492   ≤ cle 11167  2c2 12200  ♯chash 14253  Vtxcvtx 29069  iEdgciedg 29070  UPGraphcupgr 29153  USPGraphcuspgr 29221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fv 6500  df-upgr 29155  df-uspgr 29223

This theorem is referenced by:  uspgrupgrushgr  29252  uspgruhgr  29257  usgrupgr  29258  uspgrun  29261  uspgrunop  29262  uspgredg2vtxeu  29293  1loopgrnb0  29576  uspgr2wlkeq  29719  uspgrn2crct  29881  wlkiswwlks2  29948  wlkiswwlks  29949  wlklnwwlkn  29957  clwlkclwwlk  30077  wlk2v2e  30232  isuspgrim0  48140  isuspgrimlem  48141  upgrimwlklem5  48147  upgrimwlk  48148  grlimprclnbgr  48242  grlimprclnbgrvtx  48245  grlimgredgex  48246  uspgropssxp  48390  uspgrsprf  48392