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 )

Metamath Proof Explorer

Theorem uhgrstrrepe

Proof