This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gropd

Description: If any representation of a graph with vertices V and edges E has a certain property ps , then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E ) has this property. (Contributed by AV, 11-Oct-2020)

Ref Expression
Hypotheses gropd.g ⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) )
gropd.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
gropd.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
Assertion gropd ( 𝜑 → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 )

Proof

Step Hyp Ref Expression
1 gropd.g ⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) )
2 gropd.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
3 gropd.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
4 opex ⊢ ⟨ 𝑉 , 𝐸 ⟩ ∈ V
5 4 a1i ⊢ ( 𝜑 → ⟨ 𝑉 , 𝐸 ⟩ ∈ V )
6 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
7 opiedgfv ⊢ ( ( 𝑉 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
8 6 7 jca ⊢ ( ( 𝑉 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
9 2 3 8 syl2anc ⊢ ( 𝜑 → ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
10 nfcv ⊢ Ⅎ 𝑔 ⟨ 𝑉 , 𝐸 ⟩
11 nfv ⊢ Ⅎ 𝑔 ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
12 nfsbc1v ⊢ Ⅎ 𝑔 [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓
13 11 12 nfim ⊢ Ⅎ 𝑔 ( ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 )
14 fveqeq2 ⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( Vtx ‘ 𝑔 ) = 𝑉 ↔ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ) )
15 fveqeq2 ⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( iEdg ‘ 𝑔 ) = 𝐸 ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
16 14 15 anbi12d ⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) ↔ ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) ) )
17 sbceq1a ⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( 𝜓 ↔ [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 ) )
18 16 17 imbi12d ⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) ↔ ( ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 ) ) )
19 10 13 18 spcgf ⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ V → ( ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) → ( ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 ) ) )
20 5 1 9 19 syl3c ⊢ ( 𝜑 → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 )