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

Metamath Proof Explorer

Theorem 1wlkdlem2

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

Ref Expression
Hypotheses 1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
1wlkd.l ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
1wlkd.j ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
Assertion 1wlkdlem2 ( 𝜑 → 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2 1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3 1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4 1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5 1wlkd.l ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
6 1wlkd.j ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
7 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
8 3 7 syl ⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ { 𝑋 } )
10 9 5 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝑉 )
12 prssg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝐽 ) ) ↔ { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) ) )
13 3 11 12 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝐽 ) ) ↔ { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) ) )
14 6 13 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝐽 ) ) )
15 14 simpld ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) )
16 10 15 pm2.61dane ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) )