Metamath Proof Explorer

Theorem erdszelem5

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 erdszelem5 ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )

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 1 2 3 erdszelem3 ⊢ ( 𝐴 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ‘ 𝐴 ) = sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) , ℝ , < ) )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 ‘ 𝐴 ) = sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) , ℝ , < ) )
7 snex ⊢ { 𝐴 } ∈ V
8 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
9 8 fdmi ⊢ dom ♯ = V
10 7 9 eleqtrri ⊢ { 𝐴 } ∈ dom ♯
11 1 2 3 4 erdszelem4 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → { 𝐴 } ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } )
12 inelcm ⊢ ( ( { 𝐴 } ∈ dom ♯ ∧ { 𝐴 } ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) → ( dom ♯ ∩ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ )
13 10 11 12 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( dom ♯ ∩ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ )
14 imadisj ⊢ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) = ∅ ↔ ( dom ♯ ∩ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) = ∅ )
15 14 necon3bii ⊢ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ ↔ ( dom ♯ ∩ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ )
16 13 15 sylibr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ )
17 eqid ⊢ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
18 17 erdszelem2 ⊢ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ∈ Fin ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℕ )
19 18 simpli ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ∈ Fin
20 18 simpri ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℕ
21 nnssre ⊢ ℕ ⊆ ℝ
22 20 21 sstri ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℝ
23 ltso ⊢ < Or ℝ
24 fisupcl ⊢ ( ( < Or ℝ ∧ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ∈ Fin ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℝ ) ) → sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) , ℝ , < ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
25 23 24 mpan ⊢ ( ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ∈ Fin ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ⊆ ℝ ) → sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) , ℝ , < ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
26 19 22 25 mp3an13 ⊢ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ≠ ∅ → sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) , ℝ , < ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
27 16 26 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) , ℝ , < ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
28 6 27 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )