Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  upgruhgr Structured version   Visualization version   GIF version

Theorem upgruhgr 25899
 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.
StepHypRef Expression
1 eqid 2621 . . . 4 (Vtx‘𝐺) = (Vtx‘𝐺)
2 eqid 2621 . . . 4 (iEdg‘𝐺) = (iEdg‘𝐺)
31, 2upgrf 25884 . . 3 (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) ≤ 2})
4 ssrab2 3668 . . 3 {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})
5 fss 6015 . . 3 (((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
63, 4, 5sylancl 693 . 2 (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
71, 2isuhgr 25858 . 2 (𝐺 ∈ UPGraph → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})))
86, 7mpbird 247 1 (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1987  {crab 2911   ∖ cdif 3553   ⊆ wss 3556  ∅c0 3893  𝒫 cpw 4132  {csn 4150   class class class wbr 4615  dom cdm 5076  ⟶wf 5845  ‘cfv 5849   ≤ cle 10022  2c2 11017  #chash 13060  Vtxcvtx 25781  iEdgciedg 25782   UHGraph cuhgr 25854   UPGraph cupgr 25878 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4751 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3419  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-fv 5857  df-uhgr 25856  df-upgr 25880 This theorem is referenced by:  umgruhgr  25901  upgrle2  25902  usgruhgr  25978  subupgr  26079  upgrspan  26085  upgrewlkle2  26379  upgredginwlk  26408  wlkiswwlks1  26629  wlkiswwlksupgr2  26639  eulerpathpr  26973  eulercrct  26975
 Copyright terms: Public domain W3C validator