Theorem opstrgric

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) (Revised by AV, 4-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		opstrgric.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
2		opstrgric.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		simpl	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → 𝐺 ∈ UHGraph )
22	21	adantr	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐺 ∈ UHGraph )
23		simpr	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → 𝐻 ∈ V )
24	23	adantr	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐻 ∈ V )
25		simpl	⊢ ( ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
26	25	adantl	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
27		simpr	⊢ ( ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
28	27	adantl	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
29	22 24 26 28	grimidvtxedg	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) )
30		brgrici	⊢ ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐺 ≃𝑔𝑟 𝐻 )
31	29 30	syl	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐺 ≃𝑔𝑟 𝐻 )
32	3 6 13 20 31	syl22anc	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 ≃𝑔𝑟 𝐻 )