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

Metamath Proof Explorer

Theorem upgr1wlkdlem2

Description: Lemma 2 for upgr1wlkd . (Contributed by AV, 22-Jan-2021)

Ref Expression
Hypotheses upgr1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
upgr1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
upgr1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
upgr1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ ( Vtx ‘ 𝐺 ) )
upgr1wlkd.j ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } )
Assertion upgr1wlkdlem2 ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 upgr1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2 upgr1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3 upgr1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
4 upgr1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ ( Vtx ‘ 𝐺 ) )
5 upgr1wlkd.j ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } )
6 ssid ⊢ { 𝑋 , 𝑌 } ⊆ { 𝑋 , 𝑌 }
7 sseq2 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } → ( { 𝑋 , 𝑌 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) ↔ { 𝑋 , 𝑌 } ⊆ { 𝑋 , 𝑌 } ) )
8 7 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } ) → ( { 𝑋 , 𝑌 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) ↔ { 𝑋 , 𝑌 } ⊆ { 𝑋 , 𝑌 } ) )
9 6 8 mpbiri ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } ) → { 𝑋 , 𝑌 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) )
10 5 9 mpidan ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) )