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

Metamath Proof Explorer

Theorem usgredg2vlem1

Description: Lemma 1 for usgredg2v . (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgredg2v.v ⊢ V = Vtx ⁡ G
usgredg2v.e ⊢ E = iEdg ⁡ G
usgredg2v.a ⊢ A = x ∈ dom ⁡ E | N ∈ E ⁡ x
Assertion usgredg2vlem1 ⊢ G ∈ USGraph ∧ Y ∈ A → ι z ∈ V | E ⁡ Y = z N ∈ V

Proof

Step Hyp Ref Expression
1 usgredg2v.v ⊢ V = Vtx ⁡ G
2 usgredg2v.e ⊢ E = iEdg ⁡ G
3 usgredg2v.a ⊢ A = x ∈ dom ⁡ E | N ∈ E ⁡ x
4 fveq2 ⊢ x = Y → E ⁡ x = E ⁡ Y
5 4 eleq2d ⊢ x = Y → N ∈ E ⁡ x ↔ N ∈ E ⁡ Y
6 5 3 elrab2 ⊢ Y ∈ A ↔ Y ∈ dom ⁡ E ∧ N ∈ E ⁡ Y
7 1 2 usgredgreu ⊢ G ∈ USGraph ∧ Y ∈ dom ⁡ E ∧ N ∈ E ⁡ Y → ∃! z ∈ V E ⁡ Y = N z
8 prcom ⊢ N z = z N
9 8 eqeq2i ⊢ E ⁡ Y = N z ↔ E ⁡ Y = z N
10 9 reubii ⊢ ∃! z ∈ V E ⁡ Y = N z ↔ ∃! z ∈ V E ⁡ Y = z N
11 7 10 sylib ⊢ G ∈ USGraph ∧ Y ∈ dom ⁡ E ∧ N ∈ E ⁡ Y → ∃! z ∈ V E ⁡ Y = z N
12 11 3expb ⊢ G ∈ USGraph ∧ Y ∈ dom ⁡ E ∧ N ∈ E ⁡ Y → ∃! z ∈ V E ⁡ Y = z N
13 riotacl ⊢ ∃! z ∈ V E ⁡ Y = z N → ι z ∈ V | E ⁡ Y = z N ∈ V
14 12 13 syl ⊢ G ∈ USGraph ∧ Y ∈ dom ⁡ E ∧ N ∈ E ⁡ Y → ι z ∈ V | E ⁡ Y = z N ∈ V
15 6 14 sylan2b ⊢ G ∈ USGraph ∧ Y ∈ A → ι z ∈ V | E ⁡ Y = z N ∈ V