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