Metamath Proof Explorer

Theorem usgredg2ALT

Description: Alternate proof of usgredg2 , not using umgredg2 . (Contributed by Alexander van der Vekens, 11-Aug-2017) (Revised by AV, 16-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis usgredg2.e ⊢E=iEdg⁡G
Assertion usgredg2ALT ⊢G∈USGraph∧X∈dom⁡E→E⁡X=2

Proof

Step Hyp Ref Expression
1 usgredg2.e ⊢E=iEdg⁡G
2 eqid ⊢Vtx⁡G=Vtx⁡G
3 2 1 usgrf ⊢G∈USGraph→E:dom⁡E⟶1-1x∈𝒫Vtx⁡G∖∅|x=2
4 f1f ⊢E:dom⁡E⟶1-1x∈𝒫Vtx⁡G∖∅|x=2→E:dom⁡E⟶x∈𝒫Vtx⁡G∖∅|x=2
5 3 4 syl ⊢G∈USGraph→E:dom⁡E⟶x∈𝒫Vtx⁡G∖∅|x=2
6 5 ffvelcdmda ⊢G∈USGraph∧X∈dom⁡E→E⁡X∈x∈𝒫Vtx⁡G∖∅|x=2
7 fveq2 ⊢x=E⁡X→x=E⁡X
8 7 eqeq1d ⊢x=E⁡X→x=2↔E⁡X=2
9 8 elrab ⊢E⁡X∈x∈𝒫Vtx⁡G∖∅|x=2↔E⁡X∈𝒫Vtx⁡G∖∅∧E⁡X=2
10 9 simprbi ⊢E⁡X∈x∈𝒫Vtx⁡G∖∅|x=2→E⁡X=2
11 6 10 syl ⊢G∈USGraph∧X∈dom⁡E→E⁡X=2