Theorem erdszelem6

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

	Ref	Expression
Hypotheses	erdsze.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	erdsze.f	⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
	erdszelem.k	⊢ 𝐾 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
	erdszelem.o	⊢ 𝑂 Or ℝ
Assertion	erdszelem6	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) ⟶ ℕ )

Proof

Step	Hyp	Ref	Expression
1		erdsze.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		erdsze.f	⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
3		erdszelem.k	⊢ 𝐾 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
4		erdszelem.o	⊢ 𝑂 Or ℝ
5		ltso	⊢ < Or ℝ
6	5	supex	⊢ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) ∈ V
7	6	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) ∈ V )
8	3	a1i	⊢ ( 𝜑 → 𝐾 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) ) )
9		eqid	⊢ { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) }
10	9	erdszelem2	⊢ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) } ) ∈ Fin ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) } ) ⊆ ℕ )
11	10	simpri	⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) } ) ⊆ ℕ
12	1 2 3 4	erdszelem5	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 ‘ 𝑧 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) } ) )
13	11 12	sseldi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 ‘ 𝑧 ) ∈ ℕ )
14	7 8 13	fmpt2d	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) ⟶ ℕ )