grstructd

Description: If any representation of a graph with vertices V and edges E has a certain property ps , then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E ) has this property. (Contributed by AV, 12-Oct-2020) (Revised by AV, 9-Jun-2021)

	Ref	Expression
Hypotheses	gropd.g	⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) )
	gropd.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
	gropd.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
	grstructd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
	grstructd.f	⊢ ( 𝜑 → Fun ( 𝑆 ∖ { ∅ } ) )
	grstructd.d	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝑆 ) )
	grstructd.b	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = 𝑉 )
	grstructd.e	⊢ ( 𝜑 → ( .ef ‘ 𝑆 ) = 𝐸 )
Assertion	grstructd	⊢ ( 𝜑 → [ 𝑆 / 𝑔 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		gropd.g	⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) )
2		gropd.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
3		gropd.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
4		grstructd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
5		grstructd.f	⊢ ( 𝜑 → Fun ( 𝑆 ∖ { ∅ } ) )
6		grstructd.d	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝑆 ) )
7		grstructd.b	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = 𝑉 )
8		grstructd.e	⊢ ( 𝜑 → ( .ef ‘ 𝑆 ) = 𝐸 )
9		funvtxdmge2val	⊢ ( ( Fun ( 𝑆 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝑆 ) ) → ( Vtx ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
10	5 6 9	syl2anc	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
11	10 7	eqtrd	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
12		funiedgdmge2val	⊢ ( ( Fun ( 𝑆 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝑆 ) ) → ( iEdg ‘ 𝑆 ) = ( .ef ‘ 𝑆 ) )
13	5 6 12	syl2anc	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( .ef ‘ 𝑆 ) )
14	13 8	eqtrd	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = 𝐸 )
15	11 14	jca	⊢ ( 𝜑 → ( ( Vtx ‘ 𝑆 ) = 𝑉 ∧ ( iEdg ‘ 𝑆 ) = 𝐸 ) )
16		nfcv	⊢ Ⅎ 𝑔 𝑆
17		nfv	⊢ Ⅎ 𝑔 ( ( Vtx ‘ 𝑆 ) = 𝑉 ∧ ( iEdg ‘ 𝑆 ) = 𝐸 )
18		nfsbc1v	⊢ Ⅎ 𝑔 [ 𝑆 / 𝑔 ] 𝜓
19	17 18	nfim	⊢ Ⅎ 𝑔 ( ( ( Vtx ‘ 𝑆 ) = 𝑉 ∧ ( iEdg ‘ 𝑆 ) = 𝐸 ) → [ 𝑆 / 𝑔 ] 𝜓 )
20		fveqeq2	⊢ ( 𝑔 = 𝑆 → ( ( Vtx ‘ 𝑔 ) = 𝑉 ↔ ( Vtx ‘ 𝑆 ) = 𝑉 ) )
21		fveqeq2	⊢ ( 𝑔 = 𝑆 → ( ( iEdg ‘ 𝑔 ) = 𝐸 ↔ ( iEdg ‘ 𝑆 ) = 𝐸 ) )
22	20 21	anbi12d	⊢ ( 𝑔 = 𝑆 → ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) ↔ ( ( Vtx ‘ 𝑆 ) = 𝑉 ∧ ( iEdg ‘ 𝑆 ) = 𝐸 ) ) )
23		sbceq1a	⊢ ( 𝑔 = 𝑆 → ( 𝜓 ↔ [ 𝑆 / 𝑔 ] 𝜓 ) )
24	22 23	imbi12d	⊢ ( 𝑔 = 𝑆 → ( ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) ↔ ( ( ( Vtx ‘ 𝑆 ) = 𝑉 ∧ ( iEdg ‘ 𝑆 ) = 𝐸 ) → [ 𝑆 / 𝑔 ] 𝜓 ) ) )
25	16 19 24	spcgf	⊢ ( 𝑆 ∈ 𝑋 → ( ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) → ( ( ( Vtx ‘ 𝑆 ) = 𝑉 ∧ ( iEdg ‘ 𝑆 ) = 𝐸 ) → [ 𝑆 / 𝑔 ] 𝜓 ) ) )
26	4 1 15 25	syl3c	⊢ ( 𝜑 → [ 𝑆 / 𝑔 ] 𝜓 )

Metamath Proof Explorer

Theorem grstructd

Proof