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 ⊢ φ → ∀ g Vtx ⁡ g = V ∧ iEdg ⁡ g = E → ψ
gropd.v ⊢ φ → V ∈ U
gropd.e ⊢ φ → E ∈ W
grstructd.s ⊢ φ → S ∈ X
grstructd.f ⊢ φ → Fun ⁡ S ∖ ∅
grstructd.d ⊢ φ → 2 ≤ dom ⁡ S
grstructd.b ⊢ φ → Base S = V
grstructd.e ⊢ φ → ef ⁡ S = E
Assertion grstructd ⊢ φ → [˙S / g]˙ ψ

Proof

Step Hyp Ref Expression
1 gropd.g ⊢ φ → ∀ g Vtx ⁡ g = V ∧ iEdg ⁡ g = E → ψ
2 gropd.v ⊢ φ → V ∈ U
3 gropd.e ⊢ φ → E ∈ W
4 grstructd.s ⊢ φ → S ∈ X
5 grstructd.f ⊢ φ → Fun ⁡ S ∖ ∅
6 grstructd.d ⊢ φ → 2 ≤ dom ⁡ S
7 grstructd.b ⊢ φ → Base S = V
8 grstructd.e ⊢ φ → ef ⁡ S = E
9 funvtxdmge2val ⊢ Fun ⁡ S ∖ ∅ ∧ 2 ≤ dom ⁡ S → Vtx ⁡ S = Base S
10 5 6 9 syl2anc ⊢ φ → Vtx ⁡ S = Base S
11 10 7 eqtrd ⊢ φ → Vtx ⁡ S = V
12 funiedgdmge2val ⊢ Fun ⁡ S ∖ ∅ ∧ 2 ≤ dom ⁡ S → iEdg ⁡ S = ef ⁡ S
13 5 6 12 syl2anc ⊢ φ → iEdg ⁡ S = ef ⁡ S
14 13 8 eqtrd ⊢ φ → iEdg ⁡ S = E
15 11 14 jca ⊢ φ → Vtx ⁡ S = V ∧ iEdg ⁡ S = E
16 nfcv ⊢ Ⅎ _ g S
17 nfv ⊢ Ⅎ g Vtx ⁡ S = V ∧ iEdg ⁡ S = E
18 nfsbc1v ⊢ Ⅎ g [˙S / g]˙ ψ
19 17 18 nfim ⊢ Ⅎ g Vtx ⁡ S = V ∧ iEdg ⁡ S = E → [˙S / g]˙ ψ
20 fveqeq2 ⊢ g = S → Vtx ⁡ g = V ↔ Vtx ⁡ S = V
21 fveqeq2 ⊢ g = S → iEdg ⁡ g = E ↔ iEdg ⁡ S = E
22 20 21 anbi12d ⊢ g = S → Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↔ Vtx ⁡ S = V ∧ iEdg ⁡ S = E
23 sbceq1a ⊢ g = S → ψ ↔ [˙S / g]˙ ψ
24 22 23 imbi12d ⊢ g = S → Vtx ⁡ g = V ∧ iEdg ⁡ g = E → ψ ↔ Vtx ⁡ S = V ∧ iEdg ⁡ S = E → [˙S / g]˙ ψ
25 16 19 24 spcgf ⊢ S ∈ X → ∀ g Vtx ⁡ g = V ∧ iEdg ⁡ g = E → ψ → Vtx ⁡ S = V ∧ iEdg ⁡ S = E → [˙S / g]˙ ψ
26 4 1 15 25 syl3c ⊢ φ → [˙S / g]˙ ψ