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

Metamath Proof Explorer

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 ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 𝑌 = { 𝑁 , 𝑧 } ) ∈ 𝑉 )