Theorem uspgrushgr

Description: A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020) (Revised by AV, 15-Oct-2020)

	Ref	Expression
Assertion	uspgrushgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph )

Proof

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