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

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 ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )

Proof

Step Hyp Ref Expression
1 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 2 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
4 1 3 syl ⊢ ( 𝐺 ∈ USGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
5 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6 5 2 usgredgreu ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } )
7 6 3expia ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) )
8 7 3adant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) )
9 eleq2 ⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑌 ∈ 𝐸 ↔ 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
10 eqeq1 ⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝐸 = { 𝑌 , 𝑦 } ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) )
11 10 reubidv ⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ↔ ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) )
12 9 11 imbi12d ⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ↔ ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) )
13 12 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ↔ ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) )
14 8 13 mpbird ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) )
15 14 3exp ⊢ ( 𝐺 ∈ USGraph → ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ) ) )
16 15 rexlimdv ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ) )
17 4 16 sylbid ⊢ ( 𝐺 ∈ USGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ) )
18 17 3imp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )