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-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
4 f1f ⊢ E : dom ⁡ E ⟶ 1-1 x ∈ 𝒫 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 ffvelrnda ⊢ 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