Theorem upgruhgr 29305

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 2764	. . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2764	. . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	upgrf 29289	. . 3 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
4		ssrab2 4035	. . 3 ⊢ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})
5		fss 6710	. . 3 ⊢ (((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
6	3, 4, 5	sylancl 595	. 2 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
7	1, 2	isuhgr 29263	. 2 ⊢ (𝐺 ∈ UPGraph → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})))
8	6, 7	mpbird 259	1 ⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph)

Syntax hints:   → wi 4   ∈ wcel 2144  {crab 3416   ∖ cdif 3903   ⊆ wss 3906  ∅c0 4287  𝒫 cpw 4557  {csn 4584   class class class wbr 5102  dom cdm 5649  ⟶wf 6519  ‘cfv 6523   ≤ cle 11219  2c2 12274  ♯chash 14345  Vtxcvtx 29199  iEdgciedg 29200  UHGraphcuhgr 29259  UPGraphcupgr 29283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-nul 5258

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3458  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-fv 6531  df-uhgr 29261  df-upgr 29285

This theorem is referenced by:  umgruhgr  29307  upgrle2  29308  edglnl  29346  numedglnl  29347  uspgruhgr  29387  usgruhgr  29389  subupgr  29490  upgrspan  29496  upgrreslem  29507  upgrres  29509  finsumvtxdg2ssteplem1  29748  finsumvtxdg2size  29753  upgrewlkle2  29809  upgredginwlk  29838  wlkiswwlks1  30069  wlkiswwlksupgr2  30079  eulerpathpr  30444  eulercrct  30446  upgracycumgr  35508  isubgrupgr  48497