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