Metamath Proof Explorer

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 sselid ⊒ ( ( πœ‘ ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) β†’ ( 𝐾 β€˜ 𝑧 ) ∈ β„• )
14 7 8 13 fmpt2d ⊒ ( πœ‘ β†’ 𝐾 : ( 1 ... 𝑁 ) ⟢ β„• )