Metamath Proof Explorer

Theorem erdszelem8

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 ℝ
erdszelem.a ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝑁 ) )
erdszelem.b ⊢ ( 𝜑 → 𝐵 ∈ ( 1 ... 𝑁 ) )
erdszelem.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion erdszelem8 ( 𝜑 → ( ( 𝐾 ‘ 𝐴 ) = ( 𝐾 ‘ 𝐵 ) → ¬ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) )

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 erdszelem.a ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝑁 ) )
6 erdszelem.b ⊢ ( 𝜑 → 𝐵 ∈ ( 1 ... 𝑁 ) )
7 erdszelem.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
8 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
9 ffun ⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → Fun ♯ )
10 8 9 ax-mp ⊢ Fun ♯
11 1 2 3 4 erdszelem5 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
12 5 11 mpdan ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) )
13 fvelima ⊢ ( ( Fun ♯ ∧ ( 𝐾 ‘ 𝐴 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) ) → ∃ 𝑓 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ( ♯ ‘ 𝑓 ) = ( 𝐾 ‘ 𝐴 ) )
14 10 12 13 sylancr ⊢ ( 𝜑 → ∃ 𝑓 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ( ♯ ‘ 𝑓 ) = ( 𝐾 ‘ 𝐴 ) )
15 eqid ⊢ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
16 15 erdszelem1 ⊢ ( 𝑓 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ↔ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) )
17 fzfid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 1 ... 𝐴 ) ∈ Fin )
18 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝑓 ⊆ ( 1 ... 𝐴 ) )
19 ssfi ⊢ ( ( ( 1 ... 𝐴 ) ∈ Fin ∧ 𝑓 ⊆ ( 1 ... 𝐴 ) ) → 𝑓 ∈ Fin )
20 17 18 19 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝑓 ∈ Fin )
21 hashcl ⊢ ( 𝑓 ∈ Fin → ( ♯ ‘ 𝑓 ) ∈ ℕ0 )
22 20 21 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ ‘ 𝑓 ) ∈ ℕ0 )
23 22 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ ‘ 𝑓 ) ∈ ℝ )
24 eqid ⊢ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) }
25 24 erdszelem2 ⊢ ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ∈ Fin ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ⊆ ℕ )
26 25 simpri ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ⊆ ℕ
27 nnssre ⊢ ℕ ⊆ ℝ
28 26 27 sstri ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ⊆ ℝ
29 28 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ⊆ ℝ )
30 5 elfzelzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
31 6 elfzelzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
32 elfznn ⊢ ( 𝐴 ∈ ( 1 ... 𝑁 ) → 𝐴 ∈ ℕ )
33 5 32 syl ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
34 33 nnred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
35 elfznn ⊢ ( 𝐵 ∈ ( 1 ... 𝑁 ) → 𝐵 ∈ ℕ )
36 6 35 syl ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
37 36 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
38 34 37 7 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
39 eluz2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ↔ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) )
40 30 31 38 39 syl3anbrc ⊢ ( 𝜑 → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
41 fzss2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝐵 ) )
42 40 41 syl ⊢ ( 𝜑 → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝐵 ) )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝐵 ) )
44 18 43 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝑓 ⊆ ( 1 ... 𝐵 ) )
45 elfz1end ⊢ ( 𝐵 ∈ ℕ ↔ 𝐵 ∈ ( 1 ... 𝐵 ) )
46 36 45 sylib ⊢ ( 𝜑 → 𝐵 ∈ ( 1 ... 𝐵 ) )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝐵 ∈ ( 1 ... 𝐵 ) )
48 47 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → { 𝐵 } ⊆ ( 1 ... 𝐵 ) )
49 44 48 unssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝑓 ∪ { 𝐵 } ) ⊆ ( 1 ... 𝐵 ) )
50 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) )
51 f1f ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
52 2 51 syl ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
54 elfzuz3 ⊢ ( 𝐴 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) )
55 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝑁 ) )
56 5 54 55 3syl ⊢ ( 𝜑 → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝑁 ) )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝑁 ) )
58 18 57 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝑓 ⊆ ( 1 ... 𝑁 ) )
59 fzssuz ⊢ ( 1 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 1 )
60 uzssz ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
61 zssre ⊢ ℤ ⊆ ℝ
62 60 61 sstri ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℝ
63 59 62 sstri ⊢ ( 1 ... 𝑁 ) ⊆ ℝ
64 ltso ⊢ < Or ℝ
65 soss ⊢ ( ( 1 ... 𝑁 ) ⊆ ℝ → ( < Or ℝ → < Or ( 1 ... 𝑁 ) ) )
66 63 64 65 mp2 ⊢ < Or ( 1 ... 𝑁 )
67 soisores ⊢ ( ( ( < Or ( 1 ... 𝑁 ) ∧ 𝑂 Or ℝ ) ∧ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ ∧ 𝑓 ⊆ ( 1 ... 𝑁 ) ) ) → ( ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ↔ ∀ 𝑧 ∈ 𝑓 ∀ 𝑤 ∈ 𝑓 ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
68 66 4 67 mpanl12 ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ ∧ 𝑓 ⊆ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ↔ ∀ 𝑧 ∈ 𝑓 ∀ 𝑤 ∈ 𝑓 ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
69 53 58 68 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ↔ ∀ 𝑧 ∈ 𝑓 ∀ 𝑤 ∈ 𝑓 ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
70 50 69 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ∀ 𝑧 ∈ 𝑓 ∀ 𝑤 ∈ 𝑓 ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
71 70 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ∀ 𝑤 ∈ 𝑓 ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
72 18 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝑧 ∈ ( 1 ... 𝐴 ) )
73 elfzle2 ⊢ ( 𝑧 ∈ ( 1 ... 𝐴 ) → 𝑧 ≤ 𝐴 )
74 72 73 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝑧 ≤ 𝐴 )
75 58 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝑧 ∈ ( 1 ... 𝑁 ) )
76 63 75 sseldi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝑧 ∈ ℝ )
77 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝐴 ∈ ( 1 ... 𝑁 ) )
78 77 32 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝐴 ∈ ℕ )
79 78 nnred ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝐴 ∈ ℝ )
80 76 79 lenltd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝑧 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑧 ) )
81 74 80 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ¬ 𝐴 < 𝑧 )
82 50 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) )
83 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝐴 ∈ 𝑓 )
84 83 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝐴 ∈ 𝑓 )
85 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝑧 ∈ 𝑓 )
86 isorel ⊢ ( ( ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ ( 𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓 ) ) → ( 𝐴 < 𝑧 ↔ ( ( 𝐹 ↾ 𝑓 ) ‘ 𝐴 ) 𝑂 ( ( 𝐹 ↾ 𝑓 ) ‘ 𝑧 ) ) )
87 fvres ⊢ ( 𝐴 ∈ 𝑓 → ( ( 𝐹 ↾ 𝑓 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
88 fvres ⊢ ( 𝑧 ∈ 𝑓 → ( ( 𝐹 ↾ 𝑓 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
89 87 88 breqan12d ⊢ ( ( 𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓 ) → ( ( ( 𝐹 ↾ 𝑓 ) ‘ 𝐴 ) 𝑂 ( ( 𝐹 ↾ 𝑓 ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) ) )
90 89 adantl ⊢ ( ( ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ ( 𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓 ) ) → ( ( ( 𝐹 ↾ 𝑓 ) ‘ 𝐴 ) 𝑂 ( ( 𝐹 ↾ 𝑓 ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) ) )
91 86 90 bitrd ⊢ ( ( ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ ( 𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓 ) ) → ( 𝐴 < 𝑧 ↔ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) ) )
92 82 84 85 91 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝐴 < 𝑧 ↔ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) ) )
93 81 92 mtbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ¬ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) )
94 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) )
95 53 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
96 95 75 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
97 95 77 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
98 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝐵 ∈ ( 1 ... 𝑁 ) )
99 98 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → 𝐵 ∈ ( 1 ... 𝑁 ) )
100 95 99 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
101 sotr2 ⊢ ( ( 𝑂 Or ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) ) → ( ( ¬ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) )
102 4 101 mpan ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) → ( ( ¬ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) )
103 96 97 100 102 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( ( ¬ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) )
104 93 94 103 mp2and ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝐵 ) )
105 104 a1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) )
106 elsni ⊢ ( 𝑤 ∈ { 𝐵 } → 𝑤 = 𝐵 )
107 106 fveq2d ⊢ ( 𝑤 ∈ { 𝐵 } → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝐵 ) )
108 107 breq2d ⊢ ( 𝑤 ∈ { 𝐵 } → ( ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) )
109 108 imbi2d ⊢ ( 𝑤 ∈ { 𝐵 } → ( ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ) )
110 105 109 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ( 𝑤 ∈ { 𝐵 } → ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
111 110 ralrimiv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ∀ 𝑤 ∈ { 𝐵 } ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
112 ralunb ⊢ ( ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ↔ ( ∀ 𝑤 ∈ 𝑓 ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ∧ ∀ 𝑤 ∈ { 𝐵 } ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
113 71 111 112 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑓 ) → ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
114 113 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ∀ 𝑧 ∈ 𝑓 ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
115 49 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ) → 𝑤 ∈ ( 1 ... 𝐵 ) )
116 elfzle2 ⊢ ( 𝑤 ∈ ( 1 ... 𝐵 ) → 𝑤 ≤ 𝐵 )
117 116 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 1 ... 𝐵 ) ) → 𝑤 ≤ 𝐵 )
118 elfzelz ⊢ ( 𝑤 ∈ ( 1 ... 𝐵 ) → 𝑤 ∈ ℤ )
119 118 zred ⊢ ( 𝑤 ∈ ( 1 ... 𝐵 ) → 𝑤 ∈ ℝ )
120 119 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 1 ... 𝐵 ) ) → 𝑤 ∈ ℝ )
121 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 1 ... 𝐵 ) ) → 𝐵 ∈ ℝ )
122 120 121 lenltd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 1 ... 𝐵 ) ) → ( 𝑤 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑤 ) )
123 117 122 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 1 ... 𝐵 ) ) → ¬ 𝐵 < 𝑤 )
124 115 123 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ) → ¬ 𝐵 < 𝑤 )
125 124 pm2.21d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) ∧ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ) → ( 𝐵 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
126 125 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝐵 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
127 elsni ⊢ ( 𝑧 ∈ { 𝐵 } → 𝑧 = 𝐵 )
128 127 breq1d ⊢ ( 𝑧 ∈ { 𝐵 } → ( 𝑧 < 𝑤 ↔ 𝐵 < 𝑤 ) )
129 128 imbi1d ⊢ ( 𝑧 ∈ { 𝐵 } → ( ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝐵 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
130 129 ralbidv ⊢ ( 𝑧 ∈ { 𝐵 } → ( ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝐵 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
131 126 130 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝑧 ∈ { 𝐵 } → ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
132 131 ralrimiv ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ∀ 𝑧 ∈ { 𝐵 } ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
133 ralunb ⊢ ( ∀ 𝑧 ∈ ( 𝑓 ∪ { 𝐵 } ) ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ↔ ( ∀ 𝑧 ∈ 𝑓 ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ∧ ∀ 𝑧 ∈ { 𝐵 } ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
134 114 132 133 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ∀ 𝑧 ∈ ( 𝑓 ∪ { 𝐵 } ) ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) )
135 98 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → { 𝐵 } ⊆ ( 1 ... 𝑁 ) )
136 58 135 unssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝑓 ∪ { 𝐵 } ) ⊆ ( 1 ... 𝑁 ) )
137 soisores ⊢ ( ( ( < Or ( 1 ... 𝑁 ) ∧ 𝑂 Or ℝ ) ∧ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ ∧ ( 𝑓 ∪ { 𝐵 } ) ⊆ ( 1 ... 𝑁 ) ) ) → ( ( 𝐹 ↾ ( 𝑓 ∪ { 𝐵 } ) ) Isom < , 𝑂 ( ( 𝑓 ∪ { 𝐵 } ) , ( 𝐹 “ ( 𝑓 ∪ { 𝐵 } ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑓 ∪ { 𝐵 } ) ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
138 66 4 137 mpanl12 ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ ∧ ( 𝑓 ∪ { 𝐵 } ) ⊆ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ↾ ( 𝑓 ∪ { 𝐵 } ) ) Isom < , 𝑂 ( ( 𝑓 ∪ { 𝐵 } ) , ( 𝐹 “ ( 𝑓 ∪ { 𝐵 } ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑓 ∪ { 𝐵 } ) ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
139 53 136 138 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ( 𝐹 ↾ ( 𝑓 ∪ { 𝐵 } ) ) Isom < , 𝑂 ( ( 𝑓 ∪ { 𝐵 } ) , ( 𝐹 “ ( 𝑓 ∪ { 𝐵 } ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑓 ∪ { 𝐵 } ) ∀ 𝑤 ∈ ( 𝑓 ∪ { 𝐵 } ) ( 𝑧 < 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑂 ( 𝐹 ‘ 𝑤 ) ) ) )
140 134 139 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ↾ ( 𝑓 ∪ { 𝐵 } ) ) Isom < , 𝑂 ( ( 𝑓 ∪ { 𝐵 } ) , ( 𝐹 “ ( 𝑓 ∪ { 𝐵 } ) ) ) )
141 ssun2 ⊢ { 𝐵 } ⊆ ( 𝑓 ∪ { 𝐵 } )
142 snssg ⊢ ( 𝐵 ∈ ( 1 ... 𝐵 ) → ( 𝐵 ∈ ( 𝑓 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝑓 ∪ { 𝐵 } ) ) )
143 47 142 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐵 ∈ ( 𝑓 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝑓 ∪ { 𝐵 } ) ) )
144 141 143 mpbiri ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → 𝐵 ∈ ( 𝑓 ∪ { 𝐵 } ) )
145 24 erdszelem1 ⊢ ( ( 𝑓 ∪ { 𝐵 } ) ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ↔ ( ( 𝑓 ∪ { 𝐵 } ) ⊆ ( 1 ... 𝐵 ) ∧ ( 𝐹 ↾ ( 𝑓 ∪ { 𝐵 } ) ) Isom < , 𝑂 ( ( 𝑓 ∪ { 𝐵 } ) , ( 𝐹 “ ( 𝑓 ∪ { 𝐵 } ) ) ) ∧ 𝐵 ∈ ( 𝑓 ∪ { 𝐵 } ) ) )
146 49 140 144 145 syl3anbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝑓 ∪ { 𝐵 } ) ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } )
147 vex ⊢ 𝑓 ∈ V
148 snex ⊢ { 𝐵 } ∈ V
149 147 148 unex ⊢ ( 𝑓 ∪ { 𝐵 } ) ∈ V
150 8 fdmi ⊢ dom ♯ = V
151 149 150 eleqtrri ⊢ ( 𝑓 ∪ { 𝐵 } ) ∈ dom ♯
152 funfvima ⊢ ( ( Fun ♯ ∧ ( 𝑓 ∪ { 𝐵 } ) ∈ dom ♯ ) → ( ( 𝑓 ∪ { 𝐵 } ) ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } → ( ♯ ‘ ( 𝑓 ∪ { 𝐵 } ) ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ) )
153 10 151 152 mp2an ⊢ ( ( 𝑓 ∪ { 𝐵 } ) ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } → ( ♯ ‘ ( 𝑓 ∪ { 𝐵 } ) ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) )
154 146 153 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ ‘ ( 𝑓 ∪ { 𝐵 } ) ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) )
155 154 ne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ≠ ∅ )
156 25 simpli ⊢ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ∈ Fin
157 fimaxre2 ⊢ ( ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ⊆ ℝ ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ∈ Fin ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) 𝑤 ≤ 𝑧 )
158 29 156 157 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) 𝑤 ≤ 𝑧 )
159 34 37 ltnled ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
160 7 159 mpbid ⊢ ( 𝜑 → ¬ 𝐵 ≤ 𝐴 )
161 elfzle2 ⊢ ( 𝐵 ∈ ( 1 ... 𝐴 ) → 𝐵 ≤ 𝐴 )
162 160 161 nsyl ⊢ ( 𝜑 → ¬ 𝐵 ∈ ( 1 ... 𝐴 ) )
163 162 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ¬ 𝐵 ∈ ( 1 ... 𝐴 ) )
164 18 163 ssneldd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ¬ 𝐵 ∈ 𝑓 )
165 hashunsng ⊢ ( 𝐵 ∈ ( 1 ... 𝑁 ) → ( ( 𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓 ) → ( ♯ ‘ ( 𝑓 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
166 98 165 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ( 𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓 ) → ( ♯ ‘ ( 𝑓 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
167 20 164 166 mp2and ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ ‘ ( 𝑓 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
168 167 154 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑓 ) + 1 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) )
169 suprub ⊢ ( ( ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ⊆ ℝ ∧ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) 𝑤 ≤ 𝑧 ) ∧ ( ( ♯ ‘ 𝑓 ) + 1 ) ∈ ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) ) → ( ( ♯ ‘ 𝑓 ) + 1 ) ≤ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) , ℝ , < ) )
170 29 155 158 168 169 syl31anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑓 ) + 1 ) ≤ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) , ℝ , < ) )
171 1 2 3 erdszelem3 ⊢ ( 𝐵 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ‘ 𝐵 ) = sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) , ℝ , < ) )
172 6 171 syl ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐵 ) = sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) , ℝ , < ) )
173 172 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐾 ‘ 𝐵 ) = sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝐵 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐵 ∈ 𝑦 ) } ) , ℝ , < ) )
174 170 173 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑓 ) + 1 ) ≤ ( 𝐾 ‘ 𝐵 ) )
175 1 2 3 4 erdszelem6 ⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) ⟶ ℕ )
176 175 6 ffvelrnd ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐵 ) ∈ ℕ )
177 176 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐾 ‘ 𝐵 ) ∈ ℕ )
178 177 nnnn0d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( 𝐾 ‘ 𝐵 ) ∈ ℕ0 )
179 nn0ltp1le ⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( 𝐾 ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑓 ) < ( 𝐾 ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝑓 ) + 1 ) ≤ ( 𝐾 ‘ 𝐵 ) ) )
180 22 178 179 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑓 ) < ( 𝐾 ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝑓 ) + 1 ) ≤ ( 𝐾 ‘ 𝐵 ) ) )
181 174 180 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ ‘ 𝑓 ) < ( 𝐾 ‘ 𝐵 ) )
182 23 181 ltned ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) → ( ♯ ‘ 𝑓 ) ≠ ( 𝐾 ‘ 𝐵 ) )
183 182 ex ⊢ ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) → ( ♯ ‘ 𝑓 ) ≠ ( 𝐾 ‘ 𝐵 ) ) )
184 neeq1 ⊢ ( ( ♯ ‘ 𝑓 ) = ( 𝐾 ‘ 𝐴 ) → ( ( ♯ ‘ 𝑓 ) ≠ ( 𝐾 ‘ 𝐵 ) ↔ ( 𝐾 ‘ 𝐴 ) ≠ ( 𝐾 ‘ 𝐵 ) ) )
185 184 imbi2d ⊢ ( ( ♯ ‘ 𝑓 ) = ( 𝐾 ‘ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) → ( ♯ ‘ 𝑓 ) ≠ ( 𝐾 ‘ 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) → ( 𝐾 ‘ 𝐴 ) ≠ ( 𝐾 ‘ 𝐵 ) ) ) )
186 183 185 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑓 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑓 ) Isom < , 𝑂 ( 𝑓 , ( 𝐹 “ 𝑓 ) ) ∧ 𝐴 ∈ 𝑓 ) ) → ( ( ♯ ‘ 𝑓 ) = ( 𝐾 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) → ( 𝐾 ‘ 𝐴 ) ≠ ( 𝐾 ‘ 𝐵 ) ) ) )
187 16 186 sylan2b ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ) → ( ( ♯ ‘ 𝑓 ) = ( 𝐾 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) → ( 𝐾 ‘ 𝐴 ) ≠ ( 𝐾 ‘ 𝐵 ) ) ) )
188 187 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ( ♯ ‘ 𝑓 ) = ( 𝐾 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) → ( 𝐾 ‘ 𝐴 ) ≠ ( 𝐾 ‘ 𝐵 ) ) ) )
189 14 188 mpd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) → ( 𝐾 ‘ 𝐴 ) ≠ ( 𝐾 ‘ 𝐵 ) ) )
190 189 necon2bd ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐴 ) = ( 𝐾 ‘ 𝐵 ) → ¬ ( 𝐹 ‘ 𝐴 ) 𝑂 ( 𝐹 ‘ 𝐵 ) ) )