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

Metamath Proof Explorer

Theorem 1pthdlem1

Description: Lemma 1 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 1pthdlem1 Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2 1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3 fun0 ⊢ Fun ∅
4 2 fveq2i ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 ”⟩ )
5 s1len ⊢ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) = 1
6 4 5 eqtri ⊢ ( ♯ ‘ 𝐹 ) = 1
7 6 oveq2i ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ..^ 1 )
8 fzo0 ⊢ ( 1 ..^ 1 ) = ∅
9 7 8 eqtri ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ∅
10 9 reseq2i ⊢ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 𝑃 ↾ ∅ )
11 res0 ⊢ ( 𝑃 ↾ ∅ ) = ∅
12 10 11 eqtri ⊢ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅
13 12 cnveqi ⊢ ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ◡ ∅
14 cnv0 ⊢ ◡ ∅ = ∅
15 13 14 eqtri ⊢ ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅
16 15 funeqi ⊢ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ Fun ∅ )
17 3 16 mpbir ⊢ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )