| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → 𝑚 = ∅) |
| 2 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅)) |
| 3 | 2 | dmeqd 5916 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → dom (ℎ‘𝑚) = dom (ℎ‘∅)) |
| 4 | 1, 3 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ (𝑚 = ∅ → (𝑚 ∈ dom (ℎ‘𝑚) ↔ ∅ ∈ dom (ℎ‘∅))) |
| 5 | | eleq2 2830 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅)) |
| 6 | 2 | sseq2d 4016 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘∅))) |
| 7 | 5, 6 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑚 = ∅ → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))) |
| 8 | 4, 7 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑚 = ∅ → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))) |
| 9 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → 𝑚 = 𝑖) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖)) |
| 11 | 10 | dmeqd 5916 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘𝑖)) |
| 12 | 9, 11 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ 𝑖 ∈ dom (ℎ‘𝑖))) |
| 13 | | elequ2 2123 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖)) |
| 14 | 10 | sseq2d 4016 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) |
| 15 | 13, 14 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))) |
| 16 | 12, 15 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))))) |
| 17 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → 𝑚 = suc 𝑖) |
| 18 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖)) |
| 19 | 18 | dmeqd 5916 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑖)) |
| 20 | 17, 19 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖))) |
| 21 | | eleq2 2830 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖)) |
| 22 | 18 | sseq2d 4016 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))) |
| 23 | 21, 22 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑚 = suc 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
| 24 | 20, 23 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))) |
| 25 | | peano1 7910 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ ω |
| 26 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:ω⟶𝑆 ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ 𝑆) |
| 27 | 25, 26 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ 𝑆) |
| 28 | | axdc3lem2.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} |
| 29 | | fdm 6745 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠:suc 𝑛⟶𝐴 → dom 𝑠 = suc 𝑛) |
| 30 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ω → Ord 𝑛) |
| 31 | | 0elsuc 7855 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝑛 → ∅ ∈ suc
𝑛) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω → ∅
∈ suc 𝑛) |
| 33 | | peano2 7912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) |
| 34 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛)) |
| 35 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω)) |
| 36 | 34, 35 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (dom
𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc
𝑛 ∧ suc 𝑛 ∈
ω))) |
| 37 | 36 | biimprcd 250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((∅
∈ suc 𝑛 ∧ suc
𝑛 ∈ ω) →
(dom 𝑠 = suc 𝑛 → (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈
ω))) |
| 38 | 32, 33, 37 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ω → (dom
𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))) |
| 39 | 29, 38 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠:suc 𝑛⟶𝐴 → (𝑛 ∈ ω → (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈
ω))) |
| 40 | 39 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈
ω))) |
| 41 | 40 | impcom 407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)) |
| 42 | 41 | rexlimiva 3147 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)) |
| 43 | 42 | ss2abi 4067 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} |
| 44 | 28, 43 | eqsstri 4030 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} |
| 45 | 44 | sseli 3979 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ‘∅) ∈ 𝑆 → (ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}) |
| 46 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ‘∅) ∈
V |
| 47 | | dmeq 5914 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = (ℎ‘∅) → dom 𝑠 = dom (ℎ‘∅)) |
| 48 | 47 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (ℎ‘∅) → (∅ ∈ dom
𝑠 ↔ ∅ ∈ dom
(ℎ‘∅))) |
| 49 | 47 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (ℎ‘∅) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘∅) ∈
ω)) |
| 50 | 48, 49 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (ℎ‘∅) → ((∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅
∈ dom (ℎ‘∅)
∧ dom (ℎ‘∅)
∈ ω))) |
| 51 | 46, 50 | elab 3679 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈ ω)} ↔
(∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈
ω)) |
| 52 | 45, 51 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ‘∅) ∈ 𝑆 → (∅ ∈ dom
(ℎ‘∅) ∧ dom
(ℎ‘∅) ∈
ω)) |
| 53 | 52 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((ℎ‘∅) ∈ 𝑆 → ∅ ∈ dom
(ℎ‘∅)) |
| 54 | 27, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (ℎ:ω⟶𝑆 → ∅ ∈ dom (ℎ‘∅)) |
| 55 | | noel 4338 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑗 ∈
∅ |
| 56 | 55 | pm2.21i 119 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)) |
| 57 | 54, 56 | jctir 520 |
. . . . . . . . . . . 12
⊢ (ℎ:ω⟶𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))) |
| 59 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ 𝑆) |
| 60 | 59 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑖) ∈ 𝑆) |
| 61 | 60 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑖) ∈ 𝑆) |
| 62 | | suceq 6450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖) |
| 63 | 62 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖)) |
| 64 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖))) |
| 65 | 63, 64 | eleq12d 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))) |
| 66 | 65 | rspcva 3620 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ω ∧
∀𝑘 ∈ ω
(ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) |
| 67 | 66 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) |
| 68 | 44 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}) |
| 69 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ‘𝑖) ∈ V |
| 70 | | dmeq 5914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (ℎ‘𝑖) → dom 𝑠 = dom (ℎ‘𝑖)) |
| 71 | 70 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (ℎ‘𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom
(ℎ‘𝑖))) |
| 72 | 70 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (ℎ‘𝑖) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘𝑖) ∈ ω)) |
| 73 | 71, 72 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (ℎ‘𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom
(ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))) |
| 74 | 69, 73 | elab 3679 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom
(ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)) |
| 75 | 68, 74 | sylib 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)) |
| 76 | 75 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℎ‘𝑖) ∈ 𝑆 → dom (ℎ‘𝑖) ∈ ω) |
| 77 | | nnord 7895 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
(ℎ‘𝑖) ∈ ω → Ord dom (ℎ‘𝑖)) |
| 78 | | ordsucelsuc 7842 |
. . . . . . . . . . . . . . . . . 18
⊢ (Ord dom
(ℎ‘𝑖) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
| 79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
| 80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
| 81 | | dmeq 5914 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (ℎ‘𝑖) → dom 𝑥 = dom (ℎ‘𝑖)) |
| 82 | | suceq 6450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑥 = dom (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖)) |
| 83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖)) |
| 84 | 83 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (ℎ‘𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (ℎ‘𝑖))) |
| 85 | 81 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (ℎ‘𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (ℎ‘𝑖))) |
| 86 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (ℎ‘𝑖) → 𝑥 = (ℎ‘𝑖)) |
| 87 | 85, 86 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (ℎ‘𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))) |
| 88 | 84, 87 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (ℎ‘𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))) |
| 89 | 88 | rabbidv 3444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (ℎ‘𝑖) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}) |
| 90 | | axdc3lem2.3 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)}) |
| 91 | | axdc3lem2.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐴 ∈ V |
| 92 | 91, 28 | axdc3lem 10490 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑆 ∈ V |
| 93 | 92 | rabex 5339 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ∈ V |
| 94 | 89, 90, 93 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝐺‘(ℎ‘𝑖)) = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}) |
| 95 | 94 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})) |
| 96 | | dmeq 5914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (ℎ‘suc 𝑖) → dom 𝑦 = dom (ℎ‘suc 𝑖)) |
| 97 | 96 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (ℎ‘suc 𝑖) → (dom 𝑦 = suc dom (ℎ‘𝑖) ↔ dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖))) |
| 98 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (ℎ‘suc 𝑖) → (𝑦 ↾ dom (ℎ‘𝑖)) = ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖))) |
| 99 | 98 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (ℎ‘suc 𝑖) → ((𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) ↔ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))) |
| 100 | 97, 99 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (ℎ‘suc 𝑖) → ((dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) ↔ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))) |
| 101 | 100 | elrab 3692 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))) |
| 102 | 95, 101 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))) |
| 103 | 102 | simplbda 499 |
. . . . . . . . . . . . . . . . . 18
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))) |
| 104 | 103 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖)) |
| 105 | 104 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
| 106 | 80, 105 | bitr4d 282 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖))) |
| 107 | 106 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) → suc 𝑖 ∈ dom (ℎ‘suc 𝑖))) |
| 108 | 103 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) |
| 109 | | resss 6019 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) |
| 110 | | sseq1 4009 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))) |
| 111 | 109, 110 | mpbii 233 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)) |
| 112 | | elsuci 6451 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ suc 𝑖 → (𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖)) |
| 113 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) |
| 114 | | sstr2 3990 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑗) ⊆ (ℎ‘𝑖) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))) |
| 115 | 113, 114 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
| 116 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑖 → (ℎ‘𝑗) = (ℎ‘𝑖)) |
| 117 | 116 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))) |
| 118 | 117 | biimprd 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑖 → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))) |
| 119 | 118 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
| 120 | 115, 119 | jaoi 858 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
| 121 | 112, 120 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ suc 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
| 122 | 121 | com13 88 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
| 123 | 108, 111,
122 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
| 124 | 107, 123 | anim12d 609 |
. . . . . . . . . . . . 13
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))) |
| 125 | 61, 67, 124 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))) |
| 126 | 125 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))) |
| 127 | 8, 16, 24, 58, 126 | finds2 7920 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))) |
| 128 | 127 | imp 406 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))) |
| 129 | 128 | simprd 495 |
. . . . . . . 8
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) |
| 130 | 129 | expcom 413 |
. . . . . . 7
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))) |
| 131 | 130 | ralrimdv 3152 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) |
| 132 | 131 | ralrimiv 3145 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) |
| 133 | | frn 6743 |
. . . . . . . . . . . 12
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ 𝑆) |
| 134 | | ffun 6739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠:suc 𝑛⟶𝐴 → Fun 𝑠) |
| 135 | 134 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠) |
| 136 | 135 | rexlimivw 3151 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠) |
| 137 | 136 | ss2abi 4067 |
. . . . . . . . . . . . 13
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠} |
| 138 | 28, 137 | eqsstri 4030 |
. . . . . . . . . . . 12
⊢ 𝑆 ⊆ {𝑠 ∣ Fun 𝑠} |
| 139 | 133, 138 | sstrdi 3996 |
. . . . . . . . . . 11
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ Fun 𝑠}) |
| 140 | 139 | sseld 3982 |
. . . . . . . . . 10
⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → 𝑢 ∈ {𝑠 ∣ Fun 𝑠})) |
| 141 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑢 ∈ V |
| 142 | | funeq 6586 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢)) |
| 143 | 141, 142 | elab 3679 |
. . . . . . . . . 10
⊢ (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢) |
| 144 | 140, 143 | imbitrdi 251 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → Fun 𝑢)) |
| 145 | 144 | adantr 480 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → Fun 𝑢)) |
| 146 | | ffn 6736 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → ℎ Fn ω) |
| 147 | | fvelrnb 6969 |
. . . . . . . . . . . . 13
⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ ↔ ∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣)) |
| 148 | | fvelrnb 6969 |
. . . . . . . . . . . . . . 15
⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ ↔ ∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢)) |
| 149 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ω → Ord 𝑎) |
| 150 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ∈ ω → Ord 𝑏) |
| 151 | 149, 150 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord
𝑎 ∧ Ord 𝑏)) |
| 152 | | ordtri3or 6416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
𝑎 ∧ Ord 𝑏) → (𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎)) |
| 153 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 = 𝑏 → (ℎ‘𝑚) = (ℎ‘𝑏)) |
| 154 | 153 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑏))) |
| 155 | 154 | raleqbi1dv 3338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 = 𝑏 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏))) |
| 156 | 155 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏))) |
| 157 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 = 𝑎 → (ℎ‘𝑗) = (ℎ‘𝑎)) |
| 158 | 157 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑏) ↔ (ℎ‘𝑎) ⊆ (ℎ‘𝑏))) |
| 159 | 158 | rspccv 3619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑗 ∈
𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))) |
| 160 | 156, 159 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))) |
| 161 | 160 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))) |
| 162 | 161 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)) |
| 163 | 162 | orcd 874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
| 164 | 163 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
| 165 | 164 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
| 166 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑏 → (ℎ‘𝑎) = (ℎ‘𝑏)) |
| 167 | | eqimss 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)) |
| 168 | 167 | orcd 874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
| 169 | 166, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
| 170 | 169 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
| 171 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 = 𝑎 → (ℎ‘𝑚) = (ℎ‘𝑎)) |
| 172 | 171 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑎))) |
| 173 | 172 | raleqbi1dv 3338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 = 𝑎 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎))) |
| 174 | 173 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎))) |
| 175 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 = 𝑏 → (ℎ‘𝑗) = (ℎ‘𝑏)) |
| 176 | 175 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑎) ↔ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
| 177 | 176 | rspccv 3619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑗 ∈
𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
| 178 | 174, 177 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))) |
| 179 | 178 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))) |
| 180 | 179 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) |
| 181 | 180 | olcd 875 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
| 182 | 181 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
| 183 | 182 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ 𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
| 184 | 165, 170,
183 | 3jaoi 1430 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
| 185 | 152, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Ord
𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
| 186 | 151, 185 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))) |
| 187 | | sseq12 4011 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ↔ 𝑢 ⊆ 𝑣)) |
| 188 | | sseq12 4011 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((ℎ‘𝑏) = 𝑣 ∧ (ℎ‘𝑎) = 𝑢) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢)) |
| 189 | 188 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢)) |
| 190 | 187, 189 | orbi12d 919 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) ↔ (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
| 191 | 190 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
| 192 | 186, 191 | syl6 35 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
| 193 | 192 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
| 194 | 193 | exp4b 430 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ω → (𝑏 ∈ ω → ((ℎ‘𝑎) = 𝑢 → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))) |
| 195 | 194 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ω → ((ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))) |
| 196 | 195 | rexlimiv 3148 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑎 ∈
ω (ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
| 197 | 196 | rexlimdv 3153 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑎 ∈
ω (ℎ‘𝑎) = 𝑢 → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
| 198 | 148, 197 | biimtrdi 253 |
. . . . . . . . . . . . . 14
⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
| 199 | 198 | com23 86 |
. . . . . . . . . . . . 13
⊢ (ℎ Fn ω → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
| 200 | 147, 199 | sylbid 240 |
. . . . . . . . . . . 12
⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
| 201 | 200 | com24 95 |
. . . . . . . . . . 11
⊢ (ℎ Fn ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
| 202 | 201 | imp 406 |
. . . . . . . . . 10
⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
| 203 | 202 | ralrimdv 3152 |
. . . . . . . . 9
⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
| 204 | 146, 203 | sylan 580 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
| 205 | 145, 204 | jcad 512 |
. . . . . . 7
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
| 206 | 205 | ralrimiv 3145 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → ∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
| 207 | | fununi 6641 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪
ran ℎ) |
| 208 | 206, 207 | syl 17 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → Fun ∪
ran ℎ) |
| 209 | 132, 208 | syldan 591 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → Fun ∪
ran ℎ) |
| 210 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑚 ∈ V |
| 211 | 210 | eldm2 5912 |
. . . . . . . 8
⊢ (𝑚 ∈ dom ∪ ran ℎ
↔ ∃𝑢〈𝑚, 𝑢〉 ∈ ∪
ran ℎ) |
| 212 | | eluni2 4911 |
. . . . . . . . . 10
⊢
(〈𝑚, 𝑢〉 ∈ ∪ ran ℎ
↔ ∃𝑣 ∈ ran
ℎ〈𝑚, 𝑢〉 ∈ 𝑣) |
| 213 | 210, 141 | opeldm 5918 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ dom 𝑣) |
| 214 | 213 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (ℎ:ω⟶𝑆 → (〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ dom 𝑣)) |
| 215 | 133, 44 | sstrdi 3996 |
. . . . . . . . . . . . . . 15
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}) |
| 216 | | ssel 3977 |
. . . . . . . . . . . . . . . 16
⊢ (ran
ℎ ⊆ {𝑠 ∣ (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})) |
| 217 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑣 ∈ V |
| 218 | | dmeq 5914 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣) |
| 219 | 218 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣)) |
| 220 | 218 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω)) |
| 221 | 219, 220 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom
𝑣 ∧ dom 𝑣 ∈
ω))) |
| 222 | 217, 221 | elab 3679 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom
𝑣 ∧ dom 𝑣 ∈
ω)) |
| 223 | 222 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → dom 𝑣 ∈
ω) |
| 224 | 216, 223 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ (ran
ℎ ⊆ {𝑠 ∣ (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω)) |
| 225 | 215, 224 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω)) |
| 226 | 214, 225 | anim12d 609 |
. . . . . . . . . . . . 13
⊢ (ℎ:ω⟶𝑆 → ((〈𝑚, 𝑢〉 ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))) |
| 227 | | elnn 7898 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω) |
| 228 | 226, 227 | syl6 35 |
. . . . . . . . . . . 12
⊢ (ℎ:ω⟶𝑆 → ((〈𝑚, 𝑢〉 ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → 𝑚 ∈ ω)) |
| 229 | 228 | expcomd 416 |
. . . . . . . . . . 11
⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → (〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ ω))) |
| 230 | 229 | rexlimdv 3153 |
. . . . . . . . . 10
⊢ (ℎ:ω⟶𝑆 → (∃𝑣 ∈ ran ℎ〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ ω)) |
| 231 | 212, 230 | biimtrid 242 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → (〈𝑚, 𝑢〉 ∈ ∪
ran ℎ → 𝑚 ∈
ω)) |
| 232 | 231 | exlimdv 1933 |
. . . . . . . 8
⊢ (ℎ:ω⟶𝑆 → (∃𝑢〈𝑚, 𝑢〉 ∈ ∪
ran ℎ → 𝑚 ∈
ω)) |
| 233 | 211, 232 | biimtrid 242 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → (𝑚 ∈ dom ∪ ran
ℎ → 𝑚 ∈ ω)) |
| 234 | 233 | adantr 480 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran
ℎ → 𝑚 ∈ ω)) |
| 235 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ω → 𝑚 ∈
ω) |
| 236 | | fnfvelrn 7100 |
. . . . . . . . . . 11
⊢ ((ℎ Fn ω ∧ 𝑚 ∈ ω) → (ℎ‘𝑚) ∈ ran ℎ) |
| 237 | 146, 235,
236 | syl2anr 597 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑚) ∈ ran ℎ) |
| 238 | 237 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑚) ∈ ran ℎ) |
| 239 | 128 | simpld 494 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom (ℎ‘𝑚)) |
| 240 | | dmeq 5914 |
. . . . . . . . . 10
⊢ (𝑢 = (ℎ‘𝑚) → dom 𝑢 = dom (ℎ‘𝑚)) |
| 241 | 240 | eliuni 4997 |
. . . . . . . . 9
⊢ (((ℎ‘𝑚) ∈ ran ℎ ∧ 𝑚 ∈ dom (ℎ‘𝑚)) → 𝑚 ∈ ∪
𝑢 ∈ ran ℎdom 𝑢) |
| 242 | 238, 239,
241 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ ∪
𝑢 ∈ ran ℎdom 𝑢) |
| 243 | | dmuni 5925 |
. . . . . . . 8
⊢ dom ∪ ran ℎ
= ∪ 𝑢 ∈ ran ℎdom 𝑢 |
| 244 | 242, 243 | eleqtrrdi 2852 |
. . . . . . 7
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom ∪ ran
ℎ) |
| 245 | 244 | expcom 413 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran
ℎ)) |
| 246 | 234, 245 | impbid 212 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran
ℎ ↔ 𝑚 ∈ ω)) |
| 247 | 246 | eqrdv 2735 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → dom ∪
ran ℎ =
ω) |
| 248 | | rnuni 6168 |
. . . . . 6
⊢ ran ∪ ran ℎ
= ∪ 𝑠 ∈ ran ℎran 𝑠 |
| 249 | | frn 6743 |
. . . . . . . . . . . . . 14
⊢ (𝑠:suc 𝑛⟶𝐴 → ran 𝑠 ⊆ 𝐴) |
| 250 | 249 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴) |
| 251 | 250 | rexlimivw 3151 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴) |
| 252 | 251 | ss2abi 4067 |
. . . . . . . . . . 11
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} |
| 253 | 28, 252 | eqsstri 4030 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} |
| 254 | 133, 253 | sstrdi 3996 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}) |
| 255 | | ssel 3977 |
. . . . . . . . . 10
⊢ (ran
ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → 𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴})) |
| 256 | | abid 2718 |
. . . . . . . . . 10
⊢ (𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} ↔ ran 𝑠 ⊆ 𝐴) |
| 257 | 255, 256 | imbitrdi 251 |
. . . . . . . . 9
⊢ (ran
ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴)) |
| 258 | 254, 257 | syl 17 |
. . . . . . . 8
⊢ (ℎ:ω⟶𝑆 → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴)) |
| 259 | 258 | ralrimiv 3145 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴) |
| 260 | | iunss 5045 |
. . . . . . 7
⊢ (∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴 ↔ ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴) |
| 261 | 259, 260 | sylibr 234 |
. . . . . 6
⊢ (ℎ:ω⟶𝑆 → ∪
𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴) |
| 262 | 248, 261 | eqsstrid 4022 |
. . . . 5
⊢ (ℎ:ω⟶𝑆 → ran ∪ ran
ℎ ⊆ 𝐴) |
| 263 | 262 | adantr 480 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ran ∪
ran ℎ ⊆ 𝐴) |
| 264 | | df-fn 6564 |
. . . . 5
⊢ (∪ ran ℎ
Fn ω ↔ (Fun ∪ ran ℎ ∧ dom ∪ ran
ℎ =
ω)) |
| 265 | | df-f 6565 |
. . . . . 6
⊢ (∪ ran ℎ:ω⟶𝐴 ↔ (∪ ran
ℎ Fn ω ∧ ran ∪ ran ℎ
⊆ 𝐴)) |
| 266 | 265 | biimpri 228 |
. . . . 5
⊢ ((∪ ran ℎ
Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran
ℎ:ω⟶𝐴) |
| 267 | 264, 266 | sylanbr 582 |
. . . 4
⊢ (((Fun
∪ ran ℎ ∧ dom ∪ ran
ℎ = ω) ∧ ran ∪ ran ℎ
⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴) |
| 268 | 209, 247,
263, 267 | syl21anc 838 |
. . 3
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∪ ran
ℎ:ω⟶𝐴) |
| 269 | | fnfvelrn 7100 |
. . . . . . . 8
⊢ ((ℎ Fn ω ∧ ∅ ∈
ω) → (ℎ‘∅) ∈ ran ℎ) |
| 270 | 146, 25, 269 | sylancl 586 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ ran ℎ) |
| 271 | 270 | adantr 480 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ∈ ran ℎ) |
| 272 | | elssuni 4937 |
. . . . . 6
⊢ ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ⊆ ∪ ran ℎ) |
| 273 | 271, 272 | syl 17 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ⊆ ∪ ran ℎ) |
| 274 | 54 | adantr 480 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∅ ∈ dom (ℎ‘∅)) |
| 275 | | funssfv 6927 |
. . . . 5
⊢ ((Fun
∪ ran ℎ ∧ (ℎ‘∅) ⊆ ∪ ran ℎ
∧ ∅ ∈ dom (ℎ‘∅)) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅)) |
| 276 | 209, 273,
274, 275 | syl3anc 1373 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran
ℎ‘∅) = ((ℎ‘∅)‘∅)) |
| 277 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶) |
| 278 | 277 | rexlimivw 3151 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶) |
| 279 | 278 | ss2abi 4067 |
. . . . . . . . 9
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} |
| 280 | 28, 279 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} |
| 281 | 133, 280 | sstrdi 3996 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}) |
| 282 | | ssel 3977 |
. . . . . . . 8
⊢ (ran
ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶})) |
| 283 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑠 = (ℎ‘∅) → (𝑠‘∅) = ((ℎ‘∅)‘∅)) |
| 284 | 283 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑠 = (ℎ‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((ℎ‘∅)‘∅) = 𝐶)) |
| 285 | 46, 284 | elab 3679 |
. . . . . . . 8
⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((ℎ‘∅)‘∅) = 𝐶) |
| 286 | 282, 285 | imbitrdi 251 |
. . . . . . 7
⊢ (ran
ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶)) |
| 287 | 281, 286 | syl 17 |
. . . . . 6
⊢ (ℎ:ω⟶𝑆 → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶)) |
| 288 | 287 | adantr 480 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶)) |
| 289 | 271, 288 | mpd 15 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅)‘∅) = 𝐶) |
| 290 | 276, 289 | eqtrd 2777 |
. . 3
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran
ℎ‘∅) = 𝐶) |
| 291 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑘 ℎ:ω⟶𝑆 |
| 292 | | nfra1 3284 |
. . . . 5
⊢
Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) |
| 293 | 291, 292 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑘(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) |
| 294 | 133 | ad2antrr 726 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ran ℎ ⊆ 𝑆) |
| 295 | | peano2 7912 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
| 296 | | fnfvelrn 7100 |
. . . . . . . . 9
⊢ ((ℎ Fn ω ∧ suc 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ) |
| 297 | 146, 295,
296 | syl2an 596 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ) |
| 298 | 297 | adantlr 715 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ) |
| 299 | 239 | expcom 413 |
. . . . . . . . 9
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (ℎ‘𝑚))) |
| 300 | 299 | ralrimiv 3145 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚)) |
| 301 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 = suc 𝑘 → 𝑚 = suc 𝑘) |
| 302 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑚 = suc 𝑘 → (ℎ‘𝑚) = (ℎ‘suc 𝑘)) |
| 303 | 302 | dmeqd 5916 |
. . . . . . . . . . 11
⊢ (𝑚 = suc 𝑘 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑘)) |
| 304 | 301, 303 | eleq12d 2835 |
. . . . . . . . . 10
⊢ (𝑚 = suc 𝑘 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
| 305 | 304 | rspcv 3618 |
. . . . . . . . 9
⊢ (suc
𝑘 ∈ ω →
(∀𝑚 ∈ ω
𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
| 306 | 295, 305 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ω →
(∀𝑚 ∈ ω
𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
| 307 | 300, 306 | mpan9 506 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) |
| 308 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛)) |
| 309 | 308 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((dom
𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛) |
| 310 | 29, 309 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛) |
| 311 | | ordsucelsuc 7842 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
𝑛 → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛)) |
| 312 | 30, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ω → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛)) |
| 313 | 312 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ω → (suc
𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛)) |
| 314 | | rsp 3247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑘 ∈
𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑘 ∈ 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) |
| 315 | 313, 314 | syl9r 78 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑘 ∈
𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))) |
| 316 | 315 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑘 ∈ suc 𝑛 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))) |
| 317 | 310, 316 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))) |
| 318 | 317 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠:suc 𝑛⟶𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))) |
| 319 | 318 | com24 95 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠:suc 𝑛⟶𝐴 → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))) |
| 320 | 319 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))) |
| 321 | 320 | 3adant2 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))) |
| 322 | 321 | impcom 407 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) |
| 323 | 322 | rexlimiva 3147 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) |
| 324 | 323 | ss2abi 4067 |
. . . . . . . . . . 11
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} |
| 325 | 28, 324 | eqsstri 4030 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} |
| 326 | | sstr 3992 |
. . . . . . . . . 10
⊢ ((ran
ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) |
| 327 | 325, 326 | mpan2 691 |
. . . . . . . . 9
⊢ (ran
ℎ ⊆ 𝑆 → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) |
| 328 | 327 | sseld 3982 |
. . . . . . . 8
⊢ (ran
ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})) |
| 329 | | fvex 6919 |
. . . . . . . . 9
⊢ (ℎ‘suc 𝑘) ∈ V |
| 330 | | dmeq 5914 |
. . . . . . . . . . 11
⊢ (𝑠 = (ℎ‘suc 𝑘) → dom 𝑠 = dom (ℎ‘suc 𝑘)) |
| 331 | 330 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑠 = (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
| 332 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘)) |
| 333 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
| 334 | 333 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝐹‘(𝑠‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘))) |
| 335 | 332, 334 | eleq12d 2835 |
. . . . . . . . . 10
⊢ (𝑠 = (ℎ‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
| 336 | 331, 335 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑠 = (ℎ‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))) |
| 337 | 329, 336 | elab 3679 |
. . . . . . . 8
⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
| 338 | 328, 337 | imbitrdi 251 |
. . . . . . 7
⊢ (ran
ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))) |
| 339 | 294, 298,
307, 338 | syl3c 66 |
. . . . . 6
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))) |
| 340 | 209 | adantr 480 |
. . . . . . . 8
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → Fun ∪ ran ℎ) |
| 341 | | elssuni 4937 |
. . . . . . . . . 10
⊢ ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ) |
| 342 | 297, 341 | syl 17 |
. . . . . . . . 9
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ) |
| 343 | 342 | adantlr 715 |
. . . . . . . 8
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ) |
| 344 | | funssfv 6927 |
. . . . . . . 8
⊢ ((Fun
∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran
ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘)) |
| 345 | 340, 343,
307, 344 | syl3anc 1373 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘)) |
| 346 | 215 | sseld 3982 |
. . . . . . . . . . . . . . 15
⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})) |
| 347 | 330 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (ℎ‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom
(ℎ‘suc 𝑘))) |
| 348 | 330 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (ℎ‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘suc 𝑘) ∈ ω)) |
| 349 | 347, 348 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (ℎ‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom
(ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))) |
| 350 | 329, 349 | elab 3679 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom
(ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)) |
| 351 | 346, 350 | imbitrdi 251 |
. . . . . . . . . . . . . 14
⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))) |
| 352 | 351 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))) |
| 353 | 297, 352 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (∅ ∈ dom
(ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)) |
| 354 | 353 | simprd 495 |
. . . . . . . . . . 11
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → dom (ℎ‘suc 𝑘) ∈ ω) |
| 355 | | nnord 7895 |
. . . . . . . . . . 11
⊢ (dom
(ℎ‘suc 𝑘) ∈ ω → Ord dom
(ℎ‘suc 𝑘)) |
| 356 | | ordtr 6398 |
. . . . . . . . . . 11
⊢ (Ord dom
(ℎ‘suc 𝑘) → Tr dom (ℎ‘suc 𝑘)) |
| 357 | | trsuc 6471 |
. . . . . . . . . . . 12
⊢ ((Tr dom
(ℎ‘suc 𝑘) ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → 𝑘 ∈ dom (ℎ‘suc 𝑘)) |
| 358 | 357 | ex 412 |
. . . . . . . . . . 11
⊢ (Tr dom
(ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
| 359 | 354, 355,
356, 358 | 4syl 19 |
. . . . . . . . . 10
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
| 360 | 359 | adantlr 715 |
. . . . . . . . 9
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
| 361 | 307, 360 | mpd 15 |
. . . . . . . 8
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (ℎ‘suc 𝑘)) |
| 362 | | funssfv 6927 |
. . . . . . . 8
⊢ ((Fun
∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ ∧ 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
| 363 | 340, 343,
361, 362 | syl3anc 1373 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
| 364 | | simpl 482 |
. . . . . . . 8
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran
ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘)) |
| 365 | | simpr 484 |
. . . . . . . . 9
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
| 366 | 365 | fveq2d 6910 |
. . . . . . . 8
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (𝐹‘(∪ ran
ℎ‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘))) |
| 367 | 364, 366 | eleq12d 2835 |
. . . . . . 7
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → ((∪ ran
ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
| 368 | 345, 363,
367 | syl2anc 584 |
. . . . . 6
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
| 369 | 339, 368 | mpbird 257 |
. . . . 5
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))) |
| 370 | 369 | ex 412 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑘 ∈ ω → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)))) |
| 371 | 293, 370 | ralrimi 3257 |
. . 3
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑘 ∈ ω (∪
ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))) |
| 372 | | vex 3484 |
. . . . . 6
⊢ ℎ ∈ V |
| 373 | 372 | rnex 7932 |
. . . . 5
⊢ ran ℎ ∈ V |
| 374 | 373 | uniex 7761 |
. . . 4
⊢ ∪ ran ℎ
∈ V |
| 375 | | feq1 6716 |
. . . . 5
⊢ (𝑔 = ∪
ran ℎ → (𝑔:ω⟶𝐴 ↔ ∪ ran ℎ:ω⟶𝐴)) |
| 376 | | fveq1 6905 |
. . . . . 6
⊢ (𝑔 = ∪
ran ℎ → (𝑔‘∅) = (∪ ran ℎ‘∅)) |
| 377 | 376 | eqeq1d 2739 |
. . . . 5
⊢ (𝑔 = ∪
ran ℎ → ((𝑔‘∅) = 𝐶 ↔ (∪ ran ℎ‘∅) = 𝐶)) |
| 378 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑔 = ∪
ran ℎ → (𝑔‘suc 𝑘) = (∪ ran ℎ‘suc 𝑘)) |
| 379 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑔 = ∪
ran ℎ → (𝑔‘𝑘) = (∪ ran ℎ‘𝑘)) |
| 380 | 379 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑔 = ∪
ran ℎ → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(∪ ran
ℎ‘𝑘))) |
| 381 | 378, 380 | eleq12d 2835 |
. . . . . 6
⊢ (𝑔 = ∪
ran ℎ → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (∪ ran
ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)))) |
| 382 | 381 | ralbidv 3178 |
. . . . 5
⊢ (𝑔 = ∪
ran ℎ → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (∪
ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)))) |
| 383 | 375, 377,
382 | 3anbi123d 1438 |
. . . 4
⊢ (𝑔 = ∪
ran ℎ → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (∪ ran
ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪
ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))))) |
| 384 | 374, 383 | spcev 3606 |
. . 3
⊢ ((∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran
ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
| 385 | 268, 290,
371, 384 | syl3anc 1373 |
. 2
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
| 386 | 385 | exlimiv 1930 |
1
⊢
(∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |