Theorem uspgrushgr 29564

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.

Step	Hyp	Ref	Expression
1		eqid 2766	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2766	. . . . 5 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	isuspgr 29539	. . . 4 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
4		ssrab2 4037	. . . . 5 ⊢ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})
5		f1ss 6788	. . . . 5 ⊢ (((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
6	4, 5	mpan2 704	. . . 4 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
7	3, 6	biimtrdi 256	. . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅})))
8	1, 2	isushgr 29448	. . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅})))
9	7, 8	sylibrd 262	. 2 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph))
10	9	pm2.43i 53	1 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {crab 3419   ∖ cdif 3905   ⊆ wss 3908  ∅c0 4289  𝒫 cpw 4567  {csn 4594   class class class wbr 5114  dom cdm 5666  –1-1→wf1 6540  ‘cfv 6543   ≤ cle 11262  2c2 12313  ♯chash 14386  Vtxcvtx 29383  iEdgciedg 29384  USHGraphcushgr 29444  USPGraphcuspgr 29535

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fv 6551  df-ushgr 29446  df-uspgr 29537

This theorem is used by:  uspgrupgrushgr  29566  usgredgedg  29617  vtxdusgrfvedg  29878  1loopgrvd2  29890  isubgr3stgr  48781