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=zN∈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∈VE⁡Y=Nz
8 prcom ⊢Nz=zN
9 8 eqeq2i ⊢E⁡Y=Nz↔E⁡Y=zN
10 9 reubii ⊢∃!z∈VE⁡Y=Nz↔∃!z∈VE⁡Y=zN
11 7 10 sylib ⊢G∈USGraph∧Y∈dom⁡E∧N∈E⁡Y→∃!z∈VE⁡Y=zN
12 11 3expb ⊢G∈USGraph∧Y∈dom⁡E∧N∈E⁡Y→∃!z∈VE⁡Y=zN
13 riotacl ⊢∃!z∈VE⁡Y=zN→ιz∈V|E⁡Y=zN∈V
14 12 13 syl ⊢G∈USGraph∧Y∈dom⁡E∧N∈E⁡Y→ιz∈V|E⁡Y=zN∈V
15 6 14 sylan2b ⊢G∈USGraph∧Y∈A→ιz∈V|E⁡Y=zN∈V