Theorem uspgredg2vlem

Description: Lemma for uspgredg2v . (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 6-Dec-2020)

	Ref	Expression
Hypotheses	uspgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uspgredg2v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	uspgredg2v.a	⊢ 𝐴 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
Assertion	uspgredg2vlem	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		uspgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uspgredg2v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		uspgredg2v.a	⊢ 𝐴 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
4		eleq2	⊢ ( 𝑒 = 𝑌 → ( 𝑁 ∈ 𝑒 ↔ 𝑁 ∈ 𝑌 ) )
5	4 3	elrab2	⊢ ( 𝑌 ∈ 𝐴 ↔ ( 𝑌 ∈ 𝐸 ∧ 𝑁 ∈ 𝑌 ) )
6		simpl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑁 ∈ 𝑌 ) ) → 𝐺 ∈ USPGraph )
7	2	eleq2i	⊢ ( 𝑌 ∈ 𝐸 ↔ 𝑌 ∈ ( Edg ‘ 𝐺 ) )
8	7	biimpi	⊢ ( 𝑌 ∈ 𝐸 → 𝑌 ∈ ( Edg ‘ 𝐺 ) )
9	8	ad2antrl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑁 ∈ 𝑌 ) ) → 𝑌 ∈ ( Edg ‘ 𝐺 ) )
10		simprr	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑁 ∈ 𝑌 ) ) → 𝑁 ∈ 𝑌 )
11	6 9 10	3jca	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑁 ∈ 𝑌 ) ) → ( 𝐺 ∈ USPGraph ∧ 𝑌 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑌 ) )
12		uspgredg2vtxeu	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑌 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑌 ) → ∃! 𝑧 ∈ ( Vtx ‘ 𝐺 ) 𝑌 = { 𝑁 , 𝑧 } )
13		reueq1	⊢ ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( ∃! 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } ↔ ∃! 𝑧 ∈ ( Vtx ‘ 𝐺 ) 𝑌 = { 𝑁 , 𝑧 } ) )
14	1 13	ax-mp	⊢ ( ∃! 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } ↔ ∃! 𝑧 ∈ ( Vtx ‘ 𝐺 ) 𝑌 = { 𝑁 , 𝑧 } )
15	12 14	sylibr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑌 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑁 ∈ 𝑌 ) → ∃! 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } )
16		riotacl	⊢ ( ∃! 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } → ( ℩ 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )
17	11 15 16	3syl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑁 ∈ 𝑌 ) ) → ( ℩ 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )
18	5 17	sylan2b	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )