Theorem strisomgrop

Description: A graph represented as an extensible structure with vertices as base set and indexed edges is isomorphic to a hypergraph represented as ordered pair with the same vertices and edges. (Contributed by AV, 11-Nov-2022)

	Ref	Expression
Hypotheses	strisomgrop.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
	strisomgrop.h	⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ }
Assertion	strisomgrop	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 IsomGr 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		strisomgrop.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
2		strisomgrop.h	⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ }
3		simp1	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 ∈ UHGraph )
4		prex	⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ∈ V
5	2 4	eqeltri	⊢ 𝐻 ∈ V
6	5	a1i	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐻 ∈ V )
7		opvtxfv	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
8	7	3adant1	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
9	1	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
10	9	a1i	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
11	2	struct2grvtx	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ 𝐻 ) = 𝑉 )
12	11	3adant1	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ 𝐻 ) = 𝑉 )
13	8 10 12	3eqtr4d	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
14		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
15	14	3adant1	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
16	1	fveq2i	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
17	16	a1i	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
18	2	struct2griedg	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐻 ) = 𝐸 )
19	18	3adant1	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐻 ) = 𝐸 )
20	15 17 19	3eqtr4d	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
21		isomgreqve	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐺 IsomGr 𝐻 )
22	3 6 13 20 21	syl22anc	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 IsomGr 𝐻 )