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

Theorem uspgrushgr 26291
 Description: A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.)
Assertion
Ref Expression
uspgrushgr (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph)

Proof of Theorem uspgrushgr
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqid 2770 . . . . 5 (Vtx‘𝐺) = (Vtx‘𝐺)
2 eqid 2770 . . . . 5 (iEdg‘𝐺) = (iEdg‘𝐺)
31, 2isuspgr 26268 . . . 4 (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
4 ssrab2 3834 . . . . 5 {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})
5 f1ss 6246 . . . . 5 (((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
64, 5mpan2 663 . . . 4 ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
73, 6syl6bi 243 . . 3 (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅})))
81, 2isushgr 26176 . . 3 (𝐺 ∈ USPGraph → (𝐺 ∈ USHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅})))
97, 8sylibrd 249 . 2 (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph))
109pm2.43i 52 1 (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2144  {crab 3064   ∖ cdif 3718   ⊆ wss 3721  ∅c0 4061  𝒫 cpw 4295  {csn 4314   class class class wbr 4784  dom cdm 5249  –1-1→wf1 6028  ‘cfv 6031   ≤ cle 10276  2c2 11271  ♯chash 13320  Vtxcvtx 26094  iEdgciedg 26095  USHGraphcushgr 26172  USPGraphcuspgr 26264 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-nul 4920 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fv 6039  df-ushgr 26174  df-uspgr 26266 This theorem is referenced by:  uspgrupgrushgr  26293  usgredgedg  26343  vtxdusgrfvedg  26621  1loopgrvd2  26633
 Copyright terms: Public domain W3C validator