Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢ (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖}) |
2 | | 0nn0 11307 |
. . . 4
⊢ 0 ∈
ℕ0 |
3 | 2 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → 0 ∈
ℕ0) |
4 | | simpl1 1064 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → 𝑅 ∈ 𝑉) |
5 | | simpl3 1066 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → 𝐹:𝑅⟶ℕ0) |
6 | | frn 6053 |
. . . . 5
⊢ (𝐹:𝑅⟶ℕ0 → ran 𝐹 ⊆
ℕ0) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → ran 𝐹 ⊆
ℕ0) |
8 | | nn0ssz 11398 |
. . . . . 6
⊢
ℕ0 ⊆ ℤ |
9 | 7, 8 | syl6ss 3615 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → ran 𝐹 ⊆ ℤ) |
10 | | fdm 6051 |
. . . . . . . 8
⊢ (𝐹:𝑅⟶ℕ0 → dom 𝐹 = 𝑅) |
11 | 5, 10 | syl 17 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → dom 𝐹 = 𝑅) |
12 | | simpl2 1065 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → 𝑅 ≠ ∅) |
13 | 11, 12 | eqnetrd 2861 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → dom 𝐹 ≠ ∅) |
14 | | dm0rn0 5342 |
. . . . . . 7
⊢ (dom
𝐹 = ∅ ↔ ran
𝐹 =
∅) |
15 | 14 | necon3bii 2846 |
. . . . . 6
⊢ (dom
𝐹 ≠ ∅ ↔ ran
𝐹 ≠
∅) |
16 | 13, 15 | sylib 208 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → ran 𝐹 ≠ ∅) |
17 | | simpr 477 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) |
18 | | suprzcl2 11778 |
. . . . 5
⊢ ((ran
𝐹 ⊆ ℤ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
19 | 9, 16, 17, 18 | syl3anc 1326 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
20 | 7, 19 | sseldd 3604 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈
ℕ0) |
21 | | vex 3203 |
. . . . . . 7
⊢ 𝑠 ∈ V |
22 | 1 | hashbc0 15709 |
. . . . . . 7
⊢ (𝑠 ∈ V → (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) = {∅}) |
23 | 21, 22 | ax-mp 5 |
. . . . . 6
⊢ (𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) = {∅} |
24 | 23 | feq2i 6037 |
. . . . 5
⊢ (𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0)⟶𝑅 ↔ 𝑓:{∅}⟶𝑅) |
25 | 24 | biimpi 206 |
. . . 4
⊢ (𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0)⟶𝑅 → 𝑓:{∅}⟶𝑅) |
26 | | simprr 796 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → 𝑓:{∅}⟶𝑅) |
27 | | 0ex 4790 |
. . . . . . 7
⊢ ∅
∈ V |
28 | 27 | snid 4208 |
. . . . . 6
⊢ ∅
∈ {∅} |
29 | | ffvelrn 6357 |
. . . . . 6
⊢ ((𝑓:{∅}⟶𝑅 ∧ ∅ ∈ {∅})
→ (𝑓‘∅)
∈ 𝑅) |
30 | 26, 28, 29 | sylancl 694 |
. . . . 5
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝑓‘∅) ∈ 𝑅) |
31 | 21 | pwid 4174 |
. . . . . 6
⊢ 𝑠 ∈ 𝒫 𝑠 |
32 | 31 | a1i 11 |
. . . . 5
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → 𝑠 ∈ 𝒫 𝑠) |
33 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → 𝐹:𝑅⟶ℕ0) |
34 | 33, 30 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝐹‘(𝑓‘∅)) ∈
ℕ0) |
35 | 34 | nn0red 11352 |
. . . . . . 7
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝐹‘(𝑓‘∅)) ∈
ℝ) |
36 | 35 | rexrd 10089 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝐹‘(𝑓‘∅)) ∈
ℝ*) |
37 | 20 | nn0red 11352 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
38 | 37 | rexrd 10089 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈
ℝ*) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → sup(ran 𝐹, ℝ, < ) ∈
ℝ*) |
40 | | hashxrcl 13148 |
. . . . . . 7
⊢ (𝑠 ∈ V → (#‘𝑠) ∈
ℝ*) |
41 | 21, 40 | mp1i 13 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (#‘𝑠) ∈
ℝ*) |
42 | 9 | adantr 481 |
. . . . . . 7
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → ran 𝐹 ⊆ ℤ) |
43 | 17 | adantr 481 |
. . . . . . 7
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) |
44 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐹:𝑅⟶ℕ0 → 𝐹 Fn 𝑅) |
45 | 33, 44 | syl 17 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → 𝐹 Fn 𝑅) |
46 | | fnfvelrn 6356 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝑅 ∧ (𝑓‘∅) ∈ 𝑅) → (𝐹‘(𝑓‘∅)) ∈ ran 𝐹) |
47 | 45, 30, 46 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝐹‘(𝑓‘∅)) ∈ ran 𝐹) |
48 | | suprzub 11779 |
. . . . . . 7
⊢ ((ran
𝐹 ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ∧ (𝐹‘(𝑓‘∅)) ∈ ran 𝐹) → (𝐹‘(𝑓‘∅)) ≤ sup(ran 𝐹, ℝ, <
)) |
49 | 42, 43, 47, 48 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝐹‘(𝑓‘∅)) ≤ sup(ran 𝐹, ℝ, <
)) |
50 | | simprl 794 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠)) |
51 | 36, 39, 41, 49, 50 | xrletrd 11993 |
. . . . 5
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝐹‘(𝑓‘∅)) ≤ (#‘𝑠)) |
52 | 28 | a1i 11 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → ∅ ∈
{∅}) |
53 | | fvex 6201 |
. . . . . . . 8
⊢ (𝑓‘∅) ∈
V |
54 | 53 | snid 4208 |
. . . . . . 7
⊢ (𝑓‘∅) ∈ {(𝑓‘∅)} |
55 | 54 | a1i 11 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (𝑓‘∅) ∈ {(𝑓‘∅)}) |
56 | | ffn 6045 |
. . . . . . 7
⊢ (𝑓:{∅}⟶𝑅 → 𝑓 Fn {∅}) |
57 | | elpreima 6337 |
. . . . . . 7
⊢ (𝑓 Fn {∅} → (∅
∈ (◡𝑓 “ {(𝑓‘∅)}) ↔ (∅ ∈
{∅} ∧ (𝑓‘∅) ∈ {(𝑓‘∅)}))) |
58 | 26, 56, 57 | 3syl 18 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → (∅ ∈ (◡𝑓 “ {(𝑓‘∅)}) ↔ (∅ ∈
{∅} ∧ (𝑓‘∅) ∈ {(𝑓‘∅)}))) |
59 | 52, 55, 58 | mpbir2and 957 |
. . . . 5
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → ∅ ∈ (◡𝑓 “ {(𝑓‘∅)})) |
60 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑐 = (𝑓‘∅) → (𝐹‘𝑐) = (𝐹‘(𝑓‘∅))) |
61 | 60 | breq1d 4663 |
. . . . . . 7
⊢ (𝑐 = (𝑓‘∅) → ((𝐹‘𝑐) ≤ (#‘𝑧) ↔ (𝐹‘(𝑓‘∅)) ≤ (#‘𝑧))) |
62 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
63 | 1 | hashbc0 15709 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) = {∅}) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) = {∅} |
65 | 64 | sseq1i 3629 |
. . . . . . . . 9
⊢ ((𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡𝑓 “ {𝑐}) ↔ {∅} ⊆ (◡𝑓 “ {𝑐})) |
66 | 27 | snss 4316 |
. . . . . . . . 9
⊢ (∅
∈ (◡𝑓 “ {𝑐}) ↔ {∅} ⊆ (◡𝑓 “ {𝑐})) |
67 | 65, 66 | bitr4i 267 |
. . . . . . . 8
⊢ ((𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡𝑓 “ {𝑐}) ↔ ∅ ∈ (◡𝑓 “ {𝑐})) |
68 | | sneq 4187 |
. . . . . . . . . 10
⊢ (𝑐 = (𝑓‘∅) → {𝑐} = {(𝑓‘∅)}) |
69 | 68 | imaeq2d 5466 |
. . . . . . . . 9
⊢ (𝑐 = (𝑓‘∅) → (◡𝑓 “ {𝑐}) = (◡𝑓 “ {(𝑓‘∅)})) |
70 | 69 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝑐 = (𝑓‘∅) → (∅ ∈ (◡𝑓 “ {𝑐}) ↔ ∅ ∈ (◡𝑓 “ {(𝑓‘∅)}))) |
71 | 67, 70 | syl5bb 272 |
. . . . . . 7
⊢ (𝑐 = (𝑓‘∅) → ((𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡𝑓 “ {𝑐}) ↔ ∅ ∈ (◡𝑓 “ {(𝑓‘∅)}))) |
72 | 61, 71 | anbi12d 747 |
. . . . . 6
⊢ (𝑐 = (𝑓‘∅) → (((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡𝑓 “ {𝑐})) ↔ ((𝐹‘(𝑓‘∅)) ≤ (#‘𝑧) ∧ ∅ ∈ (◡𝑓 “ {(𝑓‘∅)})))) |
73 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑧 = 𝑠 → (#‘𝑧) = (#‘𝑠)) |
74 | 73 | breq2d 4665 |
. . . . . . 7
⊢ (𝑧 = 𝑠 → ((𝐹‘(𝑓‘∅)) ≤ (#‘𝑧) ↔ (𝐹‘(𝑓‘∅)) ≤ (#‘𝑠))) |
75 | 74 | anbi1d 741 |
. . . . . 6
⊢ (𝑧 = 𝑠 → (((𝐹‘(𝑓‘∅)) ≤ (#‘𝑧) ∧ ∅ ∈ (◡𝑓 “ {(𝑓‘∅)})) ↔ ((𝐹‘(𝑓‘∅)) ≤ (#‘𝑠) ∧ ∅ ∈ (◡𝑓 “ {(𝑓‘∅)})))) |
76 | 72, 75 | rspc2ev 3324 |
. . . . 5
⊢ (((𝑓‘∅) ∈ 𝑅 ∧ 𝑠 ∈ 𝒫 𝑠 ∧ ((𝐹‘(𝑓‘∅)) ≤ (#‘𝑠) ∧ ∅ ∈ (◡𝑓 “ {(𝑓‘∅)}))) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡𝑓 “ {𝑐}))) |
77 | 30, 32, 51, 59, 76 | syl112anc 1330 |
. . . 4
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:{∅}⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡𝑓 “ {𝑐}))) |
78 | 25, 77 | sylanr2 685 |
. . 3
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) ≤ (#‘𝑠) ∧ 𝑓:(𝑠(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡𝑓 “ {𝑐}))) |
79 | 1, 3, 4, 5, 20, 78 | ramub 15717 |
. 2
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (0 Ramsey 𝐹) ≤ sup(ran 𝐹, ℝ, < )) |
80 | | fvelrnb 6243 |
. . . . 5
⊢ (𝐹 Fn 𝑅 → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑐 ∈ 𝑅 (𝐹‘𝑐) = sup(ran 𝐹, ℝ, < ))) |
81 | 5, 44, 80 | 3syl 18 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑐 ∈ 𝑅 (𝐹‘𝑐) = sup(ran 𝐹, ℝ, < ))) |
82 | 19, 81 | mpbid 222 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → ∃𝑐 ∈ 𝑅 (𝐹‘𝑐) = sup(ran 𝐹, ℝ, < )) |
83 | 2 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → 0 ∈
ℕ0) |
84 | | simpll1 1100 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → 𝑅 ∈ 𝑉) |
85 | | simpll3 1102 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → 𝐹:𝑅⟶ℕ0) |
86 | | nnm1nn0 11334 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑐) ∈ ℕ → ((𝐹‘𝑐) − 1) ∈
ℕ0) |
87 | 86 | ad2antll 765 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → ((𝐹‘𝑐) − 1) ∈
ℕ0) |
88 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑐 ∈ V |
89 | 27, 88 | f1osn 6176 |
. . . . . . . . . . . 12
⊢
{〈∅, 𝑐〉}:{∅}–1-1-onto→{𝑐} |
90 | | f1of 6137 |
. . . . . . . . . . . 12
⊢
({〈∅, 𝑐〉}:{∅}–1-1-onto→{𝑐} → {〈∅, 𝑐〉}:{∅}⟶{𝑐}) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . 11
⊢
{〈∅, 𝑐〉}:{∅}⟶{𝑐} |
92 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → 𝑐 ∈ 𝑅) |
93 | 92 | snssd 4340 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → {𝑐} ⊆ 𝑅) |
94 | | fss 6056 |
. . . . . . . . . . 11
⊢
(({〈∅, 𝑐〉}:{∅}⟶{𝑐} ∧ {𝑐} ⊆ 𝑅) → {〈∅, 𝑐〉}:{∅}⟶𝑅) |
95 | 91, 93, 94 | sylancr 695 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → {〈∅,
𝑐〉}:{∅}⟶𝑅) |
96 | | ovex 6678 |
. . . . . . . . . . . 12
⊢
(1...((𝐹‘𝑐) − 1)) ∈
V |
97 | 1 | hashbc0 15709 |
. . . . . . . . . . . 12
⊢
((1...((𝐹‘𝑐) − 1)) ∈ V → ((1...((𝐹‘𝑐) − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) = {∅}) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((1...((𝐹‘𝑐) − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) = {∅} |
99 | 98 | feq2i 6037 |
. . . . . . . . . 10
⊢
({〈∅, 𝑐〉}:((1...((𝐹‘𝑐) − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0)⟶𝑅 ↔ {〈∅, 𝑐〉}:{∅}⟶𝑅) |
100 | 95, 99 | sylibr 224 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → {〈∅,
𝑐〉}:((1...((𝐹‘𝑐) − 1))(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0)⟶𝑅) |
101 | 64 | sseq1i 3629 |
. . . . . . . . . . 11
⊢ ((𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡{〈∅, 𝑐〉} “ {𝑑}) ↔ {∅} ⊆ (◡{〈∅, 𝑐〉} “ {𝑑})) |
102 | 27 | snss 4316 |
. . . . . . . . . . 11
⊢ (∅
∈ (◡{〈∅, 𝑐〉} “ {𝑑}) ↔ {∅} ⊆
(◡{〈∅, 𝑐〉} “ {𝑑})) |
103 | 101, 102 | bitr4i 267 |
. . . . . . . . . 10
⊢ ((𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡{〈∅, 𝑐〉} “ {𝑑}) ↔ ∅ ∈ (◡{〈∅, 𝑐〉} “ {𝑑})) |
104 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (1...((𝐹‘𝑐) − 1)) ∈ Fin) |
105 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → 𝑧 ⊆ (1...((𝐹‘𝑐) − 1))) |
106 | | ssdomg 8001 |
. . . . . . . . . . . . . . 15
⊢
((1...((𝐹‘𝑐) − 1)) ∈ Fin → (𝑧 ⊆ (1...((𝐹‘𝑐) − 1)) → 𝑧 ≼ (1...((𝐹‘𝑐) − 1)))) |
107 | 104, 105,
106 | sylc 65 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → 𝑧 ≼ (1...((𝐹‘𝑐) − 1))) |
108 | | ssfi 8180 |
. . . . . . . . . . . . . . . 16
⊢
(((1...((𝐹‘𝑐) − 1)) ∈ Fin ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1))) → 𝑧 ∈ Fin) |
109 | 104, 105,
108 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → 𝑧 ∈ Fin) |
110 | | hashdom 13168 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ Fin ∧ (1...((𝐹‘𝑐) − 1)) ∈ Fin) →
((#‘𝑧) ≤
(#‘(1...((𝐹‘𝑐) − 1))) ↔ 𝑧 ≼ (1...((𝐹‘𝑐) − 1)))) |
111 | 109, 104,
110 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → ((#‘𝑧) ≤ (#‘(1...((𝐹‘𝑐) − 1))) ↔ 𝑧 ≼ (1...((𝐹‘𝑐) − 1)))) |
112 | 107, 111 | mpbird 247 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (#‘𝑧) ≤ (#‘(1...((𝐹‘𝑐) − 1)))) |
113 | 87 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → ((𝐹‘𝑐) − 1) ∈
ℕ0) |
114 | | hashfz1 13134 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑐) − 1) ∈ ℕ0
→ (#‘(1...((𝐹‘𝑐) − 1))) = ((𝐹‘𝑐) − 1)) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (#‘(1...((𝐹‘𝑐) − 1))) = ((𝐹‘𝑐) − 1)) |
116 | 112, 115 | breqtrd 4679 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (#‘𝑧) ≤ ((𝐹‘𝑐) − 1)) |
117 | | hashcl 13147 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ Fin →
(#‘𝑧) ∈
ℕ0) |
118 | 109, 117 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (#‘𝑧) ∈
ℕ0) |
119 | 5 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → (𝐹‘𝑐) ∈
ℕ0) |
120 | 119 | adantrr 753 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → (𝐹‘𝑐) ∈
ℕ0) |
121 | 120 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (𝐹‘𝑐) ∈
ℕ0) |
122 | | nn0ltlem1 11437 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑧) ∈
ℕ0 ∧ (𝐹‘𝑐) ∈ ℕ0) →
((#‘𝑧) < (𝐹‘𝑐) ↔ (#‘𝑧) ≤ ((𝐹‘𝑐) − 1))) |
123 | 118, 121,
122 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → ((#‘𝑧) < (𝐹‘𝑐) ↔ (#‘𝑧) ≤ ((𝐹‘𝑐) − 1))) |
124 | 116, 123 | mpbird 247 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (#‘𝑧) < (𝐹‘𝑐)) |
125 | 27, 88 | fvsn 6446 |
. . . . . . . . . . . . . . 15
⊢
({〈∅, 𝑐〉}‘∅) = 𝑐 |
126 | | f1ofn 6138 |
. . . . . . . . . . . . . . . . 17
⊢
({〈∅, 𝑐〉}:{∅}–1-1-onto→{𝑐} → {〈∅, 𝑐〉} Fn {∅}) |
127 | | elpreima 6337 |
. . . . . . . . . . . . . . . . 17
⊢
({〈∅, 𝑐〉} Fn {∅} → (∅ ∈
(◡{〈∅, 𝑐〉} “ {𝑑}) ↔ (∅ ∈ {∅} ∧
({〈∅, 𝑐〉}‘∅) ∈ {𝑑}))) |
128 | 89, 126, 127 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∈ (◡{〈∅, 𝑐〉} “ {𝑑}) ↔ (∅ ∈
{∅} ∧ ({〈∅, 𝑐〉}‘∅) ∈ {𝑑})) |
129 | 128 | simprbi 480 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ (◡{〈∅, 𝑐〉} “ {𝑑}) → ({〈∅, 𝑐〉}‘∅) ∈
{𝑑}) |
130 | 125, 129 | syl5eqelr 2706 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ (◡{〈∅, 𝑐〉} “ {𝑑}) → 𝑐 ∈ {𝑑}) |
131 | | elsni 4194 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ {𝑑} → 𝑐 = 𝑑) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . 13
⊢ (∅
∈ (◡{〈∅, 𝑐〉} “ {𝑑}) → 𝑐 = 𝑑) |
133 | 132 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (∅
∈ (◡{〈∅, 𝑐〉} “ {𝑑}) → (𝐹‘𝑐) = (𝐹‘𝑑)) |
134 | 133 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (∅
∈ (◡{〈∅, 𝑐〉} “ {𝑑}) → ((#‘𝑧) < (𝐹‘𝑐) ↔ (#‘𝑧) < (𝐹‘𝑑))) |
135 | 124, 134 | syl5ibcom 235 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → (∅ ∈ (◡{〈∅, 𝑐〉} “ {𝑑}) → (#‘𝑧) < (𝐹‘𝑑))) |
136 | 103, 135 | syl5bi 232 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) ∧ (𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ (1...((𝐹‘𝑐) − 1)))) → ((𝑧(𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})0) ⊆ (◡{〈∅, 𝑐〉} “ {𝑑}) → (#‘𝑧) < (𝐹‘𝑑))) |
137 | 1, 83, 84, 85, 87, 100, 136 | ramlb 15723 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → ((𝐹‘𝑐) − 1) < (0 Ramsey 𝐹)) |
138 | | ramubcl 15722 |
. . . . . . . . . . 11
⊢ (((0
∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (sup(ran
𝐹, ℝ, < ) ∈
ℕ0 ∧ (0 Ramsey 𝐹) ≤ sup(ran 𝐹, ℝ, < ))) → (0 Ramsey 𝐹) ∈
ℕ0) |
139 | 3, 4, 5, 20, 79, 138 | syl32anc 1334 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (0 Ramsey 𝐹) ∈
ℕ0) |
140 | 139 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → (0 Ramsey 𝐹) ∈
ℕ0) |
141 | | nn0lem1lt 11442 |
. . . . . . . . 9
⊢ (((𝐹‘𝑐) ∈ ℕ0 ∧ (0 Ramsey
𝐹) ∈
ℕ0) → ((𝐹‘𝑐) ≤ (0 Ramsey 𝐹) ↔ ((𝐹‘𝑐) − 1) < (0 Ramsey 𝐹))) |
142 | 120, 140,
141 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → ((𝐹‘𝑐) ≤ (0 Ramsey 𝐹) ↔ ((𝐹‘𝑐) − 1) < (0 Ramsey 𝐹))) |
143 | 137, 142 | mpbird 247 |
. . . . . . 7
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝑐 ∈ 𝑅 ∧ (𝐹‘𝑐) ∈ ℕ)) → (𝐹‘𝑐) ≤ (0 Ramsey 𝐹)) |
144 | 143 | expr 643 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → ((𝐹‘𝑐) ∈ ℕ → (𝐹‘𝑐) ≤ (0 Ramsey 𝐹))) |
145 | 139 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → (0 Ramsey 𝐹) ∈
ℕ0) |
146 | 145 | nn0ge0d 11354 |
. . . . . . 7
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → 0 ≤ (0 Ramsey 𝐹)) |
147 | | breq1 4656 |
. . . . . . 7
⊢ ((𝐹‘𝑐) = 0 → ((𝐹‘𝑐) ≤ (0 Ramsey 𝐹) ↔ 0 ≤ (0 Ramsey 𝐹))) |
148 | 146, 147 | syl5ibrcom 237 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → ((𝐹‘𝑐) = 0 → (𝐹‘𝑐) ≤ (0 Ramsey 𝐹))) |
149 | | elnn0 11294 |
. . . . . . 7
⊢ ((𝐹‘𝑐) ∈ ℕ0 ↔ ((𝐹‘𝑐) ∈ ℕ ∨ (𝐹‘𝑐) = 0)) |
150 | 119, 149 | sylib 208 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → ((𝐹‘𝑐) ∈ ℕ ∨ (𝐹‘𝑐) = 0)) |
151 | 144, 148,
150 | mpjaod 396 |
. . . . 5
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → (𝐹‘𝑐) ≤ (0 Ramsey 𝐹)) |
152 | | breq1 4656 |
. . . . 5
⊢ ((𝐹‘𝑐) = sup(ran 𝐹, ℝ, < ) → ((𝐹‘𝑐) ≤ (0 Ramsey 𝐹) ↔ sup(ran 𝐹, ℝ, < ) ≤ (0 Ramsey 𝐹))) |
153 | 151, 152 | syl5ibcom 235 |
. . . 4
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ 𝑐 ∈ 𝑅) → ((𝐹‘𝑐) = sup(ran 𝐹, ℝ, < ) → sup(ran 𝐹, ℝ, < ) ≤ (0 Ramsey
𝐹))) |
154 | 153 | rexlimdva 3031 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (∃𝑐 ∈ 𝑅 (𝐹‘𝑐) = sup(ran 𝐹, ℝ, < ) → sup(ran 𝐹, ℝ, < ) ≤ (0 Ramsey
𝐹))) |
155 | 82, 154 | mpd 15 |
. 2
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ≤ (0 Ramsey 𝐹)) |
156 | 139 | nn0red 11352 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (0 Ramsey 𝐹) ∈ ℝ) |
157 | 156, 37 | letri3d 10179 |
. 2
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → ((0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < ) ↔ ((0 Ramsey 𝐹) ≤ sup(ran 𝐹, ℝ, < ) ∧ sup(ran 𝐹, ℝ, < ) ≤ (0 Ramsey
𝐹)))) |
158 | 79, 155, 157 | mpbir2and 957 |
1
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < )) |