Metamath Proof Explorer

Theorem erdszelem4

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 erdszelem4 ( ( 𝜑 ∧ 𝐴 ∈ ( 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 elfznn ⊢ ( 𝐴 ∈ ( 1 ... 𝑁 ) → 𝐴 ∈ ℕ )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ℕ )
7 elfz1end ⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( 1 ... 𝐴 ) )
8 6 7 sylib ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ( 1 ... 𝐴 ) )
9 8 snssd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → { 𝐴 } ⊆ ( 1 ... 𝐴 ) )
10 elsni ⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
11 elsni ⊢ ( 𝑦 ∈ { 𝐴 } → 𝑦 = 𝐴 )
12 10 11 breqan12d ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → ( 𝑥 < 𝑦 ↔ 𝐴 < 𝐴 ) )
13 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) → ( 𝑥 < 𝑦 ↔ 𝐴 < 𝐴 ) )
14 fzssuz ⊢ ( 1 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 1 )
15 uzssz ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
16 zssre ⊢ ℤ ⊆ ℝ
17 15 16 sstri ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℝ
18 14 17 sstri ⊢ ( 1 ... 𝑁 ) ⊆ ℝ
19 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ( 1 ... 𝑁 ) )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) → 𝐴 ∈ ( 1 ... 𝑁 ) )
21 18 20 sseldi ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) → 𝐴 ∈ ℝ )
22 21 ltnrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) → ¬ 𝐴 < 𝐴 )
23 22 pm2.21d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) → ( 𝐴 < 𝐴 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) )
24 13 23 sylbid ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) → ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) )
25 24 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) )
26 f1f ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
27 2 26 syl ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
29 19 snssd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → { 𝐴 } ⊆ ( 1 ... 𝑁 ) )
30 ltso ⊢ < Or ℝ
31 soss ⊢ ( ( 1 ... 𝑁 ) ⊆ ℝ → ( < Or ℝ → < Or ( 1 ... 𝑁 ) ) )
32 18 30 31 mp2 ⊢ < Or ( 1 ... 𝑁 )
33 soisores ⊢ ( ( ( < Or ( 1 ... 𝑁 ) ∧ 𝑂 Or ℝ ) ∧ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ ∧ { 𝐴 } ⊆ ( 1 ... 𝑁 ) ) ) → ( ( 𝐹 ↾ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 “ { 𝐴 } ) ) ↔ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) ) )
34 32 4 33 mpanl12 ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ ∧ { 𝐴 } ⊆ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ↾ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 “ { 𝐴 } ) ) ↔ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) ) )
35 28 29 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ↾ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 “ { 𝐴 } ) ) ↔ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) ) )
36 25 35 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ↾ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 “ { 𝐴 } ) ) )
37 snidg ⊢ ( 𝐴 ∈ ( 1 ... 𝑁 ) → 𝐴 ∈ { 𝐴 } )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ { 𝐴 } )
39 eqid ⊢ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
40 39 erdszelem1 ⊢ ( { 𝐴 } ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ↔ ( { 𝐴 } ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 “ { 𝐴 } ) ) ∧ 𝐴 ∈ { 𝐴 } ) )
41 9 36 38 40 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → { 𝐴 } ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } )