Theorem upgruhgr 28117

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 2732	. . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2732	. . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	upgrf 28101	. . 3 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
4		ssrab2 4043	. . 3 ⊢ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})
5		fss 6691	. . 3 ⊢ (((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
6	3, 4, 5	sylancl 587	. 2 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
7	1, 2	isuhgr 28075	. 2 ⊢ (𝐺 ∈ UPGraph → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})))
8	6, 7	mpbird 257	1 ⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph)

Syntax hints:   → wi 4   ∈ wcel 2107  {crab 3406   ∖ cdif 3911   ⊆ wss 3914  ∅c0 4288  𝒫 cpw 4566  {csn 4592   class class class wbr 5111  dom cdm 5639  ⟶wf 6498  ‘cfv 6502   ≤ cle 11200  2c2 12218  ♯chash 14241  Vtxcvtx 28011  iEdgciedg 28012  UHGraphcuhgr 28071  UPGraphcupgr 28095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2703  ax-nul 5269

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-rab 3407  df-v 3449  df-sbc 3744  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4289  df-if 4493  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4872  df-br 5112  df-opab 5174  df-rel 5646  df-cnv 5647  df-co 5648  df-dm 5649  df-rn 5650  df-iota 6454  df-fun 6504  df-fn 6505  df-f 6506  df-fv 6510  df-uhgr 28073  df-upgr 28097

This theorem is referenced by:  umgruhgr  28119  upgrle2  28120  edglnl  28158  numedglnl  28159  usgruhgr  28198  subupgr  28299  upgrspan  28305  upgrreslem  28316  upgrres  28318  finsumvtxdg2ssteplem1  28557  finsumvtxdg2size  28562  upgrewlkle2  28618  upgredginwlk  28648  wlkiswwlks1  28876  wlkiswwlksupgr2  28886  eulerpathpr  29248  eulercrct  29250  upgracycumgr  33835  isomuspgrlem2c  46124