Metamath Proof Explorer

Theorem uhgrstrrepe

Description: Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a hypergraph. Instead of requiring ( ph -> G Struct X ) , it would be sufficient to require ( ph -> Fun ( G \ { (/) } ) ) and ( ph -> G e. _V ) . (Contributed by AV, 18-Jan-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 16-Nov-2021)

Ref Expression
Hypotheses uhgrstrrepe.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
uhgrstrrepe.i ⊢ 𝐼 = ( .ef ‘ ndx )
uhgrstrrepe.s ⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
uhgrstrrepe.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
uhgrstrrepe.w ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
uhgrstrrepe.e ⊢ ( 𝜑 → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
Assertion uhgrstrrepe ( 𝜑 → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ UHGraph )

Proof

Step Hyp Ref Expression
1 uhgrstrrepe.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
2 uhgrstrrepe.i ⊢ 𝐼 = ( .ef ‘ ndx )
3 uhgrstrrepe.s ⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
4 uhgrstrrepe.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
5 uhgrstrrepe.w ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
6 uhgrstrrepe.e ⊢ ( 𝜑 → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
7 2 3 4 5 setsvtx ⊢ ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Base ‘ 𝐺 ) )
8 7 1 eqtr4di ⊢ ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝑉 )
9 8 pweqd ⊢ ( 𝜑 → 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝒫 𝑉 )
10 9 difeq1d ⊢ ( 𝜑 → ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
11 10 feq3d ⊢ ( 𝜑 → ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
12 6 11 mpbird ⊢ ( 𝜑 → 𝐸 : dom 𝐸 ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) )
13 2 3 4 5 setsiedg ⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝐸 )
14 13 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = dom 𝐸 )
15 13 14 feq12d ⊢ ( 𝜑 → ( ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) ) )
16 12 15 mpbird ⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) )
17 ovex ⊢ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ V
18 eqid ⊢ ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
19 eqid ⊢ ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
20 18 19 isuhgr ⊢ ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ V → ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ UHGraph ↔ ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) ) )
21 17 20 mp1i ⊢ ( 𝜑 → ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ UHGraph ↔ ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∖ { ∅ } ) ) )
22 16 21 mpbird ⊢ ( 𝜑 → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ UHGraph )