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 ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )