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	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) )