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

Metamath Proof Explorer

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 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅