Theorem upgruhgr 29681

Description: An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.)

Assertion

Ref	Expression
upgruhgr	⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph)

Proof of Theorem upgruhgr

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2761	. . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2761	. . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	upgrf 29665	. . 3 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
4		ssrab2 4026	. . 3 ⊢ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})
5		fss 6727	. . 3 ⊢ (((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
6	3, 4, 5	sylancl 598	. 2 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
7	1, 2	isuhgr 29639	. 2 ⊢ (𝐺 ∈ UPGraph → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})))
8	6, 7	mpbird 260	1 ⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {crab 3413   ∖ cdif 3896   ⊆ wss 3914  ∅c0 4279  𝒫 cpw 4557  {csn 4584   class class class wbr 5103  dom cdm 5651  ⟶wf 6535  ‘cfv 6539   ≤ cle 11345  2c2 12398  ♯chash 14475  Vtxcvtx 29575  iEdgciedg 29576  UHGraphcuhgr 29635  UPGraphcupgr 29659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3900  df-un 3902  df-ss 3915  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-fv 6547  df-uhgr 29637  df-upgr 29661

This theorem is used by:  umgruhgr  29683  upgrle2  29684  edglnl  29722  numedglnl  29723  uspgruhgr  29766  usgruhgr  29768  subupgr  29869  upgrspan  29875  upgrreslem  29886  upgrres  29888  finsumvtxdg2ssteplem1  30127  finsumvtxdg2size  30132  upgrewlkle2  30188  upgredginwlk  30217  wlkiswwlks1  30457  wlkiswwlksupgr2  30467  eulerpathpr  30842  eulercrct  30844  upgracycumgr  35919  isubgrupgr  48969