Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → [ 𝑆 / 𝑔 ] 𝜓 )