| Step | Hyp | Ref
| Expression |
| 1 | | constrsscn.1 |
. 2
⊢ (𝜑 → 𝑁 ∈ On) |
| 2 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = ∅ → (𝐶‘𝑚) = (𝐶‘∅)) |
| 3 | 2 | sseq1d 4015 |
. . 3
⊢ (𝑚 = ∅ → ((𝐶‘𝑚) ⊆ ℂ ↔ (𝐶‘∅) ⊆
ℂ)) |
| 4 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = 𝑛 → (𝐶‘𝑚) = (𝐶‘𝑛)) |
| 5 | 4 | sseq1d 4015 |
. . 3
⊢ (𝑚 = 𝑛 → ((𝐶‘𝑚) ⊆ ℂ ↔ (𝐶‘𝑛) ⊆ ℂ)) |
| 6 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = suc 𝑛 → (𝐶‘𝑚) = (𝐶‘suc 𝑛)) |
| 7 | 6 | sseq1d 4015 |
. . 3
⊢ (𝑚 = suc 𝑛 → ((𝐶‘𝑚) ⊆ ℂ ↔ (𝐶‘suc 𝑛) ⊆ ℂ)) |
| 8 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = 𝑁 → (𝐶‘𝑚) = (𝐶‘𝑁)) |
| 9 | 8 | sseq1d 4015 |
. . 3
⊢ (𝑚 = 𝑁 → ((𝐶‘𝑚) ⊆ ℂ ↔ (𝐶‘𝑁) ⊆ ℂ)) |
| 10 | | constr0.1 |
. . . . 5
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) |
| 11 | 10 | constr0 33778 |
. . . 4
⊢ (𝐶‘∅) = {0,
1} |
| 12 | | 0cn 11253 |
. . . . 5
⊢ 0 ∈
ℂ |
| 13 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 14 | | prssi 4821 |
. . . . 5
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → {0, 1} ⊆
ℂ) |
| 15 | 12, 13, 14 | mp2an 692 |
. . . 4
⊢ {0, 1}
⊆ ℂ |
| 16 | 11, 15 | eqsstri 4030 |
. . 3
⊢ (𝐶‘∅) ⊆
ℂ |
| 17 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑛 ∈ On ∧ (𝐶‘𝑛) ⊆ ℂ) → 𝑛 ∈ On) |
| 18 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝐶‘𝑛) = (𝐶‘𝑛) |
| 19 | 10, 17, 18 | constrsuc 33779 |
. . . . . . . 8
⊢ ((𝑛 ∈ On ∧ (𝐶‘𝑛) ⊆ ℂ) → (𝑥 ∈ (𝐶‘suc 𝑛) ↔ (𝑥 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))) |
| 20 | 19 | biimpa 476 |
. . . . . . 7
⊢ (((𝑛 ∈ On ∧ (𝐶‘𝑛) ⊆ ℂ) ∧ 𝑥 ∈ (𝐶‘suc 𝑛)) → (𝑥 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))) |
| 21 | 20 | simpld 494 |
. . . . . 6
⊢ (((𝑛 ∈ On ∧ (𝐶‘𝑛) ⊆ ℂ) ∧ 𝑥 ∈ (𝐶‘suc 𝑛)) → 𝑥 ∈ ℂ) |
| 22 | 21 | ex 412 |
. . . . 5
⊢ ((𝑛 ∈ On ∧ (𝐶‘𝑛) ⊆ ℂ) → (𝑥 ∈ (𝐶‘suc 𝑛) → 𝑥 ∈ ℂ)) |
| 23 | 22 | ssrdv 3989 |
. . . 4
⊢ ((𝑛 ∈ On ∧ (𝐶‘𝑛) ⊆ ℂ) → (𝐶‘suc 𝑛) ⊆ ℂ) |
| 24 | 23 | ex 412 |
. . 3
⊢ (𝑛 ∈ On → ((𝐶‘𝑛) ⊆ ℂ → (𝐶‘suc 𝑛) ⊆ ℂ)) |
| 25 | | vex 3484 |
. . . . . . 7
⊢ 𝑚 ∈ V |
| 26 | 25 | a1i 11 |
. . . . . 6
⊢ ((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) → 𝑚 ∈ V) |
| 27 | | simpl 482 |
. . . . . 6
⊢ ((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) → Lim 𝑚) |
| 28 | 10, 26, 27 | constrlim 33780 |
. . . . 5
⊢ ((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) → (𝐶‘𝑚) = ∪ 𝑜 ∈ 𝑚 (𝐶‘𝑜)) |
| 29 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑛 = 𝑜 → (𝐶‘𝑛) = (𝐶‘𝑜)) |
| 30 | 29 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑛 = 𝑜 → ((𝐶‘𝑛) ⊆ ℂ ↔ (𝐶‘𝑜) ⊆ ℂ)) |
| 31 | | simplr 769 |
. . . . . . 7
⊢ (((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) ∧ 𝑜 ∈ 𝑚) → ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) |
| 32 | | simpr 484 |
. . . . . . 7
⊢ (((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) ∧ 𝑜 ∈ 𝑚) → 𝑜 ∈ 𝑚) |
| 33 | 30, 31, 32 | rspcdva 3623 |
. . . . . 6
⊢ (((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) ∧ 𝑜 ∈ 𝑚) → (𝐶‘𝑜) ⊆ ℂ) |
| 34 | 33 | iunssd 5050 |
. . . . 5
⊢ ((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) → ∪ 𝑜 ∈ 𝑚 (𝐶‘𝑜) ⊆ ℂ) |
| 35 | 28, 34 | eqsstrd 4018 |
. . . 4
⊢ ((Lim
𝑚 ∧ ∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ) → (𝐶‘𝑚) ⊆ ℂ) |
| 36 | 35 | ex 412 |
. . 3
⊢ (Lim
𝑚 → (∀𝑛 ∈ 𝑚 (𝐶‘𝑛) ⊆ ℂ → (𝐶‘𝑚) ⊆ ℂ)) |
| 37 | 3, 5, 7, 9, 16, 24, 36 | tfinds 7881 |
. 2
⊢ (𝑁 ∈ On → (𝐶‘𝑁) ⊆ ℂ) |
| 38 | 1, 37 | syl 17 |
1
⊢ (𝜑 → (𝐶‘𝑁) ⊆ ℂ) |