Metamath Proof Explorer

Theorem usgredg2vtxeuALT

Description: Alternate proof of usgredg2vtxeu , using edgiedgb , the general translation from ( iEdgG ) to ( EdgG ) . (Contributed by AV, 18-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion usgredg2vtxeuALT ⊢ G ∈ USGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y

Proof

Step Hyp Ref Expression
1 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 2 uhgredgiedgb ⊢ G ∈ UHGraph → E ∈ Edg ⁡ G ↔ ∃ x ∈ dom ⁡ iEdg ⁡ G E = iEdg ⁡ G ⁡ x
4 1 3 syl ⊢ G ∈ USGraph → E ∈ Edg ⁡ G ↔ ∃ x ∈ dom ⁡ iEdg ⁡ G E = iEdg ⁡ G ⁡ x
5 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
6 5 2 usgredgreu ⊢ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ G ∧ Y ∈ iEdg ⁡ G ⁡ x → ∃! y ∈ Vtx ⁡ G iEdg ⁡ G ⁡ x = Y y
7 6 3expia ⊢ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ G → Y ∈ iEdg ⁡ G ⁡ x → ∃! y ∈ Vtx ⁡ G iEdg ⁡ G ⁡ x = Y y
8 7 3adant3 ⊢ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ G ∧ E = iEdg ⁡ G ⁡ x → Y ∈ iEdg ⁡ G ⁡ x → ∃! y ∈ Vtx ⁡ G iEdg ⁡ G ⁡ x = Y y
9 eleq2 ⊢ E = iEdg ⁡ G ⁡ x → Y ∈ E ↔ Y ∈ iEdg ⁡ G ⁡ x
10 eqeq1 ⊢ E = iEdg ⁡ G ⁡ x → E = Y y ↔ iEdg ⁡ G ⁡ x = Y y
11 10 reubidv ⊢ E = iEdg ⁡ G ⁡ x → ∃! y ∈ Vtx ⁡ G E = Y y ↔ ∃! y ∈ Vtx ⁡ G iEdg ⁡ G ⁡ x = Y y
12 9 11 imbi12d ⊢ E = iEdg ⁡ G ⁡ x → Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y ↔ Y ∈ iEdg ⁡ G ⁡ x → ∃! y ∈ Vtx ⁡ G iEdg ⁡ G ⁡ x = Y y
13 12 3ad2ant3 ⊢ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ G ∧ E = iEdg ⁡ G ⁡ x → Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y ↔ Y ∈ iEdg ⁡ G ⁡ x → ∃! y ∈ Vtx ⁡ G iEdg ⁡ G ⁡ x = Y y
14 8 13 mpbird ⊢ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ G ∧ E = iEdg ⁡ G ⁡ x → Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y
15 14 3exp ⊢ G ∈ USGraph → x ∈ dom ⁡ iEdg ⁡ G → E = iEdg ⁡ G ⁡ x → Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y
16 15 rexlimdv ⊢ G ∈ USGraph → ∃ x ∈ dom ⁡ iEdg ⁡ G E = iEdg ⁡ G ⁡ x → Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y
17 4 16 sylbid ⊢ G ∈ USGraph → E ∈ Edg ⁡ G → Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y
18 17 3imp ⊢ G ∈ USGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y