Theorem 1pthdlem2

Description: Lemma 2 for 1pthd . (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021)

	Ref	Expression
Hypotheses	1wlkd.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
	1wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 ”⟩
Assertion	1pthdlem2	⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2		1wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3	2	fveq2i	⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 ”⟩ )
4		s1len	⊢ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) = 1
5	3 4	eqtri	⊢ ( ♯ ‘ 𝐹 ) = 1
6	5	oveq2i	⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ..^ 1 )
7		fzo0	⊢ ( 1 ..^ 1 ) = ∅
8	6 7	eqtri	⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ∅
9	8	imaeq2i	⊢ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 𝑃 “ ∅ )
10	9	ineq2i	⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ∅ ) )
11		ima0	⊢ ( 𝑃 “ ∅ ) = ∅
12	11	ineq2i	⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ∅ ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ∅ )
13		in0	⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ∅ ) = ∅
14	12 13	eqtri	⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ∅ ) ) = ∅
15	10 14	eqtri	⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅