Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → 𝑚 = ∅) |
2 | | fveq2 6738 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅)) |
3 | 2 | dmeqd 5791 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → dom (ℎ‘𝑚) = dom (ℎ‘∅)) |
4 | 1, 3 | eleq12d 2834 |
. . . . . . . . . . . 12
⊢ (𝑚 = ∅ → (𝑚 ∈ dom (ℎ‘𝑚) ↔ ∅ ∈ dom (ℎ‘∅))) |
5 | | eleq2 2828 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅)) |
6 | 2 | sseq2d 3949 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘∅))) |
7 | 5, 6 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑚 = ∅ → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))) |
8 | 4, 7 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑚 = ∅ → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))) |
9 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → 𝑚 = 𝑖) |
10 | | fveq2 6738 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖)) |
11 | 10 | dmeqd 5791 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘𝑖)) |
12 | 9, 11 | eleq12d 2834 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ 𝑖 ∈ dom (ℎ‘𝑖))) |
13 | | elequ2 2127 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖)) |
14 | 10 | sseq2d 3949 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) |
15 | 13, 14 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))) |
16 | 12, 15 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))))) |
17 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → 𝑚 = suc 𝑖) |
18 | | fveq2 6738 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖)) |
19 | 18 | dmeqd 5791 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑖)) |
20 | 17, 19 | eleq12d 2834 |
. . . . . . . . . . . 12
⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖))) |
21 | | eleq2 2828 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖)) |
22 | 18 | sseq2d 3949 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))) |
23 | 21, 22 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑚 = suc 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
24 | 20, 23 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))) |
25 | | peano1 7688 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ ω |
26 | | ffvelrn 6923 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:ω⟶𝑆 ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ 𝑆) |
27 | 25, 26 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ 𝑆) |
28 | | axdc3lem2.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} |
29 | | fdm 6575 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠:suc 𝑛⟶𝐴 → dom 𝑠 = suc 𝑛) |
30 | | nnord 7673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ω → Ord 𝑛) |
31 | | 0elsuc 7635 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝑛 → ∅ ∈ suc
𝑛) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω → ∅
∈ suc 𝑛) |
33 | | peano2 7689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) |
34 | | eleq2 2828 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛)) |
35 | | eleq1 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω)) |
36 | 34, 35 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (dom
𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc
𝑛 ∧ suc 𝑛 ∈
ω))) |
37 | 36 | biimprcd 253 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((∅
∈ suc 𝑛 ∧ suc
𝑛 ∈ ω) →
(dom 𝑠 = suc 𝑛 → (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈
ω))) |
38 | 32, 33, 37 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ω → (dom
𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))) |
39 | 29, 38 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠:suc 𝑛⟶𝐴 → (𝑛 ∈ ω → (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈
ω))) |
40 | 39 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈
ω))) |
41 | 40 | impcom 411 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)) |
42 | 41 | rexlimiva 3210 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)) |
43 | 42 | ss2abi 3996 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} |
44 | 28, 43 | eqsstri 3951 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} |
45 | 44 | sseli 3913 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ‘∅) ∈ 𝑆 → (ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}) |
46 | | fvex 6751 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ‘∅) ∈
V |
47 | | dmeq 5789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = (ℎ‘∅) → dom 𝑠 = dom (ℎ‘∅)) |
48 | 47 | eleq2d 2825 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (ℎ‘∅) → (∅ ∈ dom
𝑠 ↔ ∅ ∈ dom
(ℎ‘∅))) |
49 | 47 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (ℎ‘∅) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘∅) ∈
ω)) |
50 | 48, 49 | anbi12d 634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (ℎ‘∅) → ((∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅
∈ dom (ℎ‘∅)
∧ dom (ℎ‘∅)
∈ ω))) |
51 | 46, 50 | elab 3602 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈ ω)} ↔
(∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈
ω)) |
52 | 45, 51 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ‘∅) ∈ 𝑆 → (∅ ∈ dom
(ℎ‘∅) ∧ dom
(ℎ‘∅) ∈
ω)) |
53 | 52 | simpld 498 |
. . . . . . . . . . . . . 14
⊢ ((ℎ‘∅) ∈ 𝑆 → ∅ ∈ dom
(ℎ‘∅)) |
54 | 27, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (ℎ:ω⟶𝑆 → ∅ ∈ dom (ℎ‘∅)) |
55 | | noel 4261 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑗 ∈
∅ |
56 | 55 | pm2.21i 119 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)) |
57 | 54, 56 | jctir 524 |
. . . . . . . . . . . 12
⊢ (ℎ:ω⟶𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))) |
58 | 57 | adantr 484 |
. . . . . . . . . . 11
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))) |
59 | | ffvelrn 6923 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ 𝑆) |
60 | 59 | ancoms 462 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑖) ∈ 𝑆) |
61 | 60 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑖) ∈ 𝑆) |
62 | | suceq 6298 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖) |
63 | 62 | fveq2d 6742 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖)) |
64 | | 2fveq3 6743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖))) |
65 | 63, 64 | eleq12d 2834 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))) |
66 | 65 | rspcva 3550 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ω ∧
∀𝑘 ∈ ω
(ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) |
67 | 66 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) |
68 | 44 | sseli 3913 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}) |
69 | | fvex 6751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ‘𝑖) ∈ V |
70 | | dmeq 5789 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (ℎ‘𝑖) → dom 𝑠 = dom (ℎ‘𝑖)) |
71 | 70 | eleq2d 2825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (ℎ‘𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom
(ℎ‘𝑖))) |
72 | 70 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (ℎ‘𝑖) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘𝑖) ∈ ω)) |
73 | 71, 72 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (ℎ‘𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom
(ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))) |
74 | 69, 73 | elab 3602 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom
(ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)) |
75 | 68, 74 | sylib 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)) |
76 | 75 | simprd 499 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℎ‘𝑖) ∈ 𝑆 → dom (ℎ‘𝑖) ∈ ω) |
77 | | nnord 7673 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
(ℎ‘𝑖) ∈ ω → Ord dom (ℎ‘𝑖)) |
78 | | ordsucelsuc 7622 |
. . . . . . . . . . . . . . . . . 18
⊢ (Ord dom
(ℎ‘𝑖) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
80 | 79 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
81 | | dmeq 5789 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (ℎ‘𝑖) → dom 𝑥 = dom (ℎ‘𝑖)) |
82 | | suceq 6298 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑥 = dom (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖)) |
84 | 83 | eqeq2d 2750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (ℎ‘𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (ℎ‘𝑖))) |
85 | 81 | reseq2d 5868 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (ℎ‘𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (ℎ‘𝑖))) |
86 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (ℎ‘𝑖) → 𝑥 = (ℎ‘𝑖)) |
87 | 85, 86 | eqeq12d 2755 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (ℎ‘𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))) |
88 | 84, 87 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (ℎ‘𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))) |
89 | 88 | rabbidv 3405 |
. . . . . . . . . . . . . . . . . . . . . 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 10093 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑆 ∈ V |
93 | 92 | rabex 5241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ∈ V |
94 | 89, 90, 93 | fvmpt 6839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝐺‘(ℎ‘𝑖)) = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}) |
95 | 94 | eleq2d 2825 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})) |
96 | | dmeq 5789 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (ℎ‘suc 𝑖) → dom 𝑦 = dom (ℎ‘suc 𝑖)) |
97 | 96 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (ℎ‘suc 𝑖) → (dom 𝑦 = suc dom (ℎ‘𝑖) ↔ dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖))) |
98 | | reseq1 5862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (ℎ‘suc 𝑖) → (𝑦 ↾ dom (ℎ‘𝑖)) = ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖))) |
99 | 98 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (ℎ‘suc 𝑖) → ((𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) ↔ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))) |
100 | 97, 99 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (ℎ‘suc 𝑖) → ((dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) ↔ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))) |
101 | 100 | elrab 3617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))) |
102 | 95, 101 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))) |
103 | 102 | simplbda 503 |
. . . . . . . . . . . . . . . . . 18
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))) |
104 | 103 | simpld 498 |
. . . . . . . . . . . . . . . . 17
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖)) |
105 | 104 | eleq2d 2825 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖))) |
106 | 80, 105 | bitr4d 285 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖))) |
107 | 106 | biimpd 232 |
. . . . . . . . . . . . . 14
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) → suc 𝑖 ∈ dom (ℎ‘suc 𝑖))) |
108 | 103 | simprd 499 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) |
109 | | resss 5893 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) |
110 | | sseq1 3942 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))) |
111 | 109, 110 | mpbii 236 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)) |
112 | | elsuci 6299 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ suc 𝑖 → (𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖)) |
113 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) |
114 | | sstr2 3924 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑗) ⊆ (ℎ‘𝑖) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))) |
115 | 113, 114 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
116 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑖 → (ℎ‘𝑗) = (ℎ‘𝑖)) |
117 | 116 | sseq1d 3948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))) |
118 | 117 | biimprd 251 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑖 → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))) |
119 | 118 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))) |
120 | 115, 119 | jaoi 857 |
. . . . . . . . . . . . . . . . 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 612 |
. . . . . . . . . . . . 13
⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))) |
125 | 61, 67, 124 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))) |
126 | 125 | ex 416 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))) |
127 | 8, 16, 24, 58, 126 | finds2 7699 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))) |
128 | 127 | imp 410 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))) |
129 | 128 | simprd 499 |
. . . . . . . 8
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) |
130 | 129 | expcom 417 |
. . . . . . 7
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))) |
131 | 130 | ralrimdv 3112 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) |
132 | 131 | ralrimiv 3107 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) |
133 | | frn 6573 |
. . . . . . . . . . . 12
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ 𝑆) |
134 | | ffun 6569 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠:suc 𝑛⟶𝐴 → Fun 𝑠) |
135 | 134 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠) |
136 | 135 | rexlimivw 3211 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠) |
137 | 136 | ss2abi 3996 |
. . . . . . . . . . . . 13
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠} |
138 | 28, 137 | eqsstri 3951 |
. . . . . . . . . . . 12
⊢ 𝑆 ⊆ {𝑠 ∣ Fun 𝑠} |
139 | 133, 138 | sstrdi 3929 |
. . . . . . . . . . 11
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ Fun 𝑠}) |
140 | 139 | sseld 3916 |
. . . . . . . . . 10
⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → 𝑢 ∈ {𝑠 ∣ Fun 𝑠})) |
141 | | vex 3427 |
. . . . . . . . . . 11
⊢ 𝑢 ∈ V |
142 | | funeq 6420 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢)) |
143 | 141, 142 | elab 3602 |
. . . . . . . . . 10
⊢ (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢) |
144 | 140, 143 | syl6ib 254 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → Fun 𝑢)) |
145 | 144 | adantr 484 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → Fun 𝑢)) |
146 | | ffn 6566 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → ℎ Fn ω) |
147 | | fvelrnb 6794 |
. . . . . . . . . . . . 13
⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ ↔ ∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣)) |
148 | | fvelrnb 6794 |
. . . . . . . . . . . . . . 15
⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ ↔ ∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢)) |
149 | | nnord 7673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ω → Ord 𝑎) |
150 | | nnord 7673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ∈ ω → Ord 𝑏) |
151 | 149, 150 | anim12i 616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord
𝑎 ∧ Ord 𝑏)) |
152 | | ordtri3or 6265 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
𝑎 ∧ Ord 𝑏) → (𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎)) |
153 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 = 𝑏 → (ℎ‘𝑚) = (ℎ‘𝑏)) |
154 | 153 | sseq2d 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑏))) |
155 | 154 | raleqbi1dv 3332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 = 𝑏 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏))) |
156 | 155 | rspcv 3547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏))) |
157 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 = 𝑎 → (ℎ‘𝑗) = (ℎ‘𝑎)) |
158 | 157 | sseq1d 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑏) ↔ (ℎ‘𝑎) ⊆ (ℎ‘𝑏))) |
159 | 158 | rspccv 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑗 ∈
𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))) |
160 | 156, 159 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))) |
161 | 160 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))) |
162 | 161 | 3imp 1113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)) |
163 | 162 | orcd 873 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
164 | 163 | 3exp 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
165 | 164 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
166 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑏 → (ℎ‘𝑎) = (ℎ‘𝑏)) |
167 | | eqimss 3973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)) |
168 | 167 | orcd 873 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
169 | 166, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
170 | 169 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
171 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 = 𝑎 → (ℎ‘𝑚) = (ℎ‘𝑎)) |
172 | 171 | sseq2d 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑎))) |
173 | 172 | raleqbi1dv 3332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 = 𝑎 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎))) |
174 | 173 | rspcv 3547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎))) |
175 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 = 𝑏 → (ℎ‘𝑗) = (ℎ‘𝑏)) |
176 | 175 | sseq1d 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑎) ↔ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
177 | 176 | rspccv 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑗 ∈
𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
178 | 174, 177 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 ∈ ω →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))) |
179 | 178 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))) |
180 | 179 | 3imp 1113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) |
181 | 180 | olcd 874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧
∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))) |
182 | 181 | 3exp 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
183 | 182 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ 𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
184 | 165, 170,
183 | 3jaoi 1429 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
185 | 152, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Ord
𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))) |
186 | 151, 185 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))) |
187 | | sseq12 3944 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ↔ 𝑢 ⊆ 𝑣)) |
188 | | sseq12 3944 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((ℎ‘𝑏) = 𝑣 ∧ (ℎ‘𝑎) = 𝑢) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢)) |
189 | 188 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢)) |
190 | 187, 189 | orbi12d 919 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) ↔ (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
191 | 190 | biimpcd 252 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
192 | 186, 191 | syl6 35 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
(∀𝑚 ∈ ω
∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
193 | 192 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
194 | 193 | exp4b 434 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ω → (𝑏 ∈ ω → ((ℎ‘𝑎) = 𝑢 → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))) |
195 | 194 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ω → ((ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))) |
196 | 195 | rexlimiv 3209 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑎 ∈
ω (ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
197 | 196 | rexlimdv 3212 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑎 ∈
ω (ℎ‘𝑎) = 𝑢 → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
198 | 148, 197 | syl6bi 256 |
. . . . . . . . . . . . . 14
⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
199 | 198 | com23 86 |
. . . . . . . . . . . . 13
⊢ (ℎ Fn ω → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
200 | 147, 199 | sylbid 243 |
. . . . . . . . . . . 12
⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
201 | 200 | com24 95 |
. . . . . . . . . . 11
⊢ (ℎ Fn ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))) |
202 | 201 | imp 410 |
. . . . . . . . . 10
⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
203 | 202 | ralrimdv 3112 |
. . . . . . . . 9
⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
204 | 146, 203 | sylan 583 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
205 | 145, 204 | jcad 516 |
. . . . . . 7
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
206 | 205 | ralrimiv 3107 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → ∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
207 | | fununi 6475 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪
ran ℎ) |
208 | 206, 207 | syl 17 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → Fun ∪
ran ℎ) |
209 | 132, 208 | syldan 594 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → Fun ∪
ran ℎ) |
210 | | vex 3427 |
. . . . . . . . 9
⊢ 𝑚 ∈ V |
211 | 210 | eldm2 5787 |
. . . . . . . 8
⊢ (𝑚 ∈ dom ∪ ran ℎ
↔ ∃𝑢〈𝑚, 𝑢〉 ∈ ∪
ran ℎ) |
212 | | eluni2 4839 |
. . . . . . . . . 10
⊢
(〈𝑚, 𝑢〉 ∈ ∪ ran ℎ
↔ ∃𝑣 ∈ ran
ℎ〈𝑚, 𝑢〉 ∈ 𝑣) |
213 | 210, 141 | opeldm 5793 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ dom 𝑣) |
214 | 213 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (ℎ:ω⟶𝑆 → (〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ dom 𝑣)) |
215 | 133, 44 | sstrdi 3929 |
. . . . . . . . . . . . . . 15
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}) |
216 | | ssel 3910 |
. . . . . . . . . . . . . . . 16
⊢ (ran
ℎ ⊆ {𝑠 ∣ (∅ ∈ dom
𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})) |
217 | | vex 3427 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑣 ∈ V |
218 | | dmeq 5789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣) |
219 | 218 | eleq2d 2825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣)) |
220 | 218 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω)) |
221 | 219, 220 | anbi12d 634 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom
𝑣 ∧ dom 𝑣 ∈
ω))) |
222 | 217, 221 | elab 3602 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom
𝑣 ∧ dom 𝑣 ∈
ω)) |
223 | 222 | simprbi 500 |
. . . . . . . . . . . . . . . 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 612 |
. . . . . . . . . . . . 13
⊢ (ℎ:ω⟶𝑆 → ((〈𝑚, 𝑢〉 ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))) |
227 | | elnn 7676 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω) |
228 | 226, 227 | syl6 35 |
. . . . . . . . . . . 12
⊢ (ℎ:ω⟶𝑆 → ((〈𝑚, 𝑢〉 ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → 𝑚 ∈ ω)) |
229 | 228 | expcomd 420 |
. . . . . . . . . . 11
⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → (〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ ω))) |
230 | 229 | rexlimdv 3212 |
. . . . . . . . . 10
⊢ (ℎ:ω⟶𝑆 → (∃𝑣 ∈ ran ℎ〈𝑚, 𝑢〉 ∈ 𝑣 → 𝑚 ∈ ω)) |
231 | 212, 230 | syl5bi 245 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → (〈𝑚, 𝑢〉 ∈ ∪
ran ℎ → 𝑚 ∈
ω)) |
232 | 231 | exlimdv 1941 |
. . . . . . . 8
⊢ (ℎ:ω⟶𝑆 → (∃𝑢〈𝑚, 𝑢〉 ∈ ∪
ran ℎ → 𝑚 ∈
ω)) |
233 | 211, 232 | syl5bi 245 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → (𝑚 ∈ dom ∪ ran
ℎ → 𝑚 ∈ ω)) |
234 | 233 | adantr 484 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran
ℎ → 𝑚 ∈ ω)) |
235 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ω → 𝑚 ∈
ω) |
236 | | fnfvelrn 6922 |
. . . . . . . . . . 11
⊢ ((ℎ Fn ω ∧ 𝑚 ∈ ω) → (ℎ‘𝑚) ∈ ran ℎ) |
237 | 146, 235,
236 | syl2anr 600 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑚) ∈ ran ℎ) |
238 | 237 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑚) ∈ ran ℎ) |
239 | 128 | simpld 498 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom (ℎ‘𝑚)) |
240 | | dmeq 5789 |
. . . . . . . . . 10
⊢ (𝑢 = (ℎ‘𝑚) → dom 𝑢 = dom (ℎ‘𝑚)) |
241 | 240 | eliuni 4926 |
. . . . . . . . 9
⊢ (((ℎ‘𝑚) ∈ ran ℎ ∧ 𝑚 ∈ dom (ℎ‘𝑚)) → 𝑚 ∈ ∪
𝑢 ∈ ran ℎdom 𝑢) |
242 | 238, 239,
241 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ ∪
𝑢 ∈ ran ℎdom 𝑢) |
243 | | dmuni 5800 |
. . . . . . . 8
⊢ dom ∪ ran ℎ
= ∪ 𝑢 ∈ ran ℎdom 𝑢 |
244 | 242, 243 | eleqtrrdi 2851 |
. . . . . . 7
⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom ∪ ran
ℎ) |
245 | 244 | expcom 417 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran
ℎ)) |
246 | 234, 245 | impbid 215 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran
ℎ ↔ 𝑚 ∈ ω)) |
247 | 246 | eqrdv 2737 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → dom ∪
ran ℎ =
ω) |
248 | | rnuni 6029 |
. . . . . 6
⊢ ran ∪ ran ℎ
= ∪ 𝑠 ∈ ran ℎran 𝑠 |
249 | | frn 6573 |
. . . . . . . . . . . . . 14
⊢ (𝑠:suc 𝑛⟶𝐴 → ran 𝑠 ⊆ 𝐴) |
250 | 249 | 3ad2ant1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴) |
251 | 250 | rexlimivw 3211 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴) |
252 | 251 | ss2abi 3996 |
. . . . . . . . . . 11
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} |
253 | 28, 252 | eqsstri 3951 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} |
254 | 133, 253 | sstrdi 3929 |
. . . . . . . . 9
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}) |
255 | | ssel 3910 |
. . . . . . . . . 10
⊢ (ran
ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → 𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴})) |
256 | | abid 2720 |
. . . . . . . . . 10
⊢ (𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} ↔ ran 𝑠 ⊆ 𝐴) |
257 | 255, 256 | syl6ib 254 |
. . . . . . . . 9
⊢ (ran
ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴)) |
258 | 254, 257 | syl 17 |
. . . . . . . 8
⊢ (ℎ:ω⟶𝑆 → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴)) |
259 | 258 | ralrimiv 3107 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴) |
260 | | iunss 4970 |
. . . . . . 7
⊢ (∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴 ↔ ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴) |
261 | 259, 260 | sylibr 237 |
. . . . . 6
⊢ (ℎ:ω⟶𝑆 → ∪
𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴) |
262 | 248, 261 | eqsstrid 3965 |
. . . . 5
⊢ (ℎ:ω⟶𝑆 → ran ∪ ran
ℎ ⊆ 𝐴) |
263 | 262 | adantr 484 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ran ∪
ran ℎ ⊆ 𝐴) |
264 | | df-fn 6403 |
. . . . 5
⊢ (∪ ran ℎ
Fn ω ↔ (Fun ∪ ran ℎ ∧ dom ∪ ran
ℎ =
ω)) |
265 | | df-f 6404 |
. . . . . 6
⊢ (∪ ran ℎ:ω⟶𝐴 ↔ (∪ ran
ℎ Fn ω ∧ ran ∪ ran ℎ
⊆ 𝐴)) |
266 | 265 | biimpri 231 |
. . . . 5
⊢ ((∪ ran ℎ
Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran
ℎ:ω⟶𝐴) |
267 | 264, 266 | sylanbr 585 |
. . . 4
⊢ (((Fun
∪ ran ℎ ∧ dom ∪ ran
ℎ = ω) ∧ ran ∪ ran ℎ
⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴) |
268 | 209, 247,
263, 267 | syl21anc 838 |
. . 3
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∪ ran
ℎ:ω⟶𝐴) |
269 | | fnfvelrn 6922 |
. . . . . . . 8
⊢ ((ℎ Fn ω ∧ ∅ ∈
ω) → (ℎ‘∅) ∈ ran ℎ) |
270 | 146, 25, 269 | sylancl 589 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ ran ℎ) |
271 | 270 | adantr 484 |
. . . . . 6
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ∈ ran ℎ) |
272 | | elssuni 4867 |
. . . . . 6
⊢ ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ⊆ ∪ ran ℎ) |
273 | 271, 272 | syl 17 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ⊆ ∪ ran ℎ) |
274 | 54 | adantr 484 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∅ ∈ dom (ℎ‘∅)) |
275 | | funssfv 6759 |
. . . . 5
⊢ ((Fun
∪ ran ℎ ∧ (ℎ‘∅) ⊆ ∪ ran ℎ
∧ ∅ ∈ dom (ℎ‘∅)) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅)) |
276 | 209, 273,
274, 275 | syl3anc 1373 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran
ℎ‘∅) = ((ℎ‘∅)‘∅)) |
277 | | simp2 1139 |
. . . . . . . . . . 11
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶) |
278 | 277 | rexlimivw 3211 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶) |
279 | 278 | ss2abi 3996 |
. . . . . . . . 9
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} |
280 | 28, 279 | eqsstri 3951 |
. . . . . . . 8
⊢ 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} |
281 | 133, 280 | sstrdi 3929 |
. . . . . . 7
⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}) |
282 | | ssel 3910 |
. . . . . . . 8
⊢ (ran
ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶})) |
283 | | fveq1 6737 |
. . . . . . . . . 10
⊢ (𝑠 = (ℎ‘∅) → (𝑠‘∅) = ((ℎ‘∅)‘∅)) |
284 | 283 | eqeq1d 2741 |
. . . . . . . . 9
⊢ (𝑠 = (ℎ‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((ℎ‘∅)‘∅) = 𝐶)) |
285 | 46, 284 | elab 3602 |
. . . . . . . 8
⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((ℎ‘∅)‘∅) = 𝐶) |
286 | 282, 285 | syl6ib 254 |
. . . . . . 7
⊢ (ran
ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶)) |
287 | 281, 286 | syl 17 |
. . . . . 6
⊢ (ℎ:ω⟶𝑆 → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶)) |
288 | 287 | adantr 484 |
. . . . 5
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶)) |
289 | 271, 288 | mpd 15 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅)‘∅) = 𝐶) |
290 | 276, 289 | eqtrd 2779 |
. . 3
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran
ℎ‘∅) = 𝐶) |
291 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑘 ℎ:ω⟶𝑆 |
292 | | nfra1 3143 |
. . . . 5
⊢
Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) |
293 | 291, 292 | nfan 1907 |
. . . 4
⊢
Ⅎ𝑘(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) |
294 | 133 | ad2antrr 726 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ran ℎ ⊆ 𝑆) |
295 | | peano2 7689 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
296 | | fnfvelrn 6922 |
. . . . . . . . 9
⊢ ((ℎ Fn ω ∧ suc 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ) |
297 | 146, 295,
296 | syl2an 599 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ) |
298 | 297 | adantlr 715 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ) |
299 | 239 | expcom 417 |
. . . . . . . . 9
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (ℎ‘𝑚))) |
300 | 299 | ralrimiv 3107 |
. . . . . . . 8
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚)) |
301 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 = suc 𝑘 → 𝑚 = suc 𝑘) |
302 | | fveq2 6738 |
. . . . . . . . . . . 12
⊢ (𝑚 = suc 𝑘 → (ℎ‘𝑚) = (ℎ‘suc 𝑘)) |
303 | 302 | dmeqd 5791 |
. . . . . . . . . . 11
⊢ (𝑚 = suc 𝑘 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑘)) |
304 | 301, 303 | eleq12d 2834 |
. . . . . . . . . 10
⊢ (𝑚 = suc 𝑘 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
305 | 304 | rspcv 3547 |
. . . . . . . . 9
⊢ (suc
𝑘 ∈ ω →
(∀𝑚 ∈ ω
𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
306 | 295, 305 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ω →
(∀𝑚 ∈ ω
𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
307 | 300, 306 | mpan9 510 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) |
308 | | eleq2 2828 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛)) |
309 | 308 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((dom
𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛) |
310 | 29, 309 | sylan 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛) |
311 | | ordsucelsuc 7622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
𝑛 → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛)) |
312 | 30, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ω → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛)) |
313 | 312 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ω → (suc
𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛)) |
314 | | rsp 3130 |
. . . . . . . . . . . . . . . . . . . . 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 416 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠:suc 𝑛⟶𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))) |
319 | 318 | com24 95 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠:suc 𝑛⟶𝐴 → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))) |
320 | 319 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))) |
321 | 320 | 3adant2 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))) |
322 | 321 | impcom 411 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) |
323 | 322 | rexlimiva 3210 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) |
324 | 323 | ss2abi 3996 |
. . . . . . . . . . 11
⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} |
325 | 28, 324 | eqsstri 3951 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} |
326 | | sstr 3925 |
. . . . . . . . . 10
⊢ ((ran
ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) |
327 | 325, 326 | mpan2 691 |
. . . . . . . . 9
⊢ (ran
ℎ ⊆ 𝑆 → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) |
328 | 327 | sseld 3916 |
. . . . . . . 8
⊢ (ran
ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})) |
329 | | fvex 6751 |
. . . . . . . . 9
⊢ (ℎ‘suc 𝑘) ∈ V |
330 | | dmeq 5789 |
. . . . . . . . . . 11
⊢ (𝑠 = (ℎ‘suc 𝑘) → dom 𝑠 = dom (ℎ‘suc 𝑘)) |
331 | 330 | eleq2d 2825 |
. . . . . . . . . 10
⊢ (𝑠 = (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘))) |
332 | | fveq1 6737 |
. . . . . . . . . . 11
⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘)) |
333 | | fveq1 6737 |
. . . . . . . . . . . 12
⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
334 | 333 | fveq2d 6742 |
. . . . . . . . . . 11
⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝐹‘(𝑠‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘))) |
335 | 332, 334 | eleq12d 2834 |
. . . . . . . . . 10
⊢ (𝑠 = (ℎ‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
336 | 331, 335 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑠 = (ℎ‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))) |
337 | 329, 336 | elab 3602 |
. . . . . . . 8
⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
338 | 328, 337 | syl6ib 254 |
. . . . . . 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 484 |
. . . . . . . 8
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → Fun ∪ ran ℎ) |
341 | | elssuni 4867 |
. . . . . . . . . 10
⊢ ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ) |
342 | 297, 341 | syl 17 |
. . . . . . . . 9
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ) |
343 | 342 | adantlr 715 |
. . . . . . . 8
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ) |
344 | | funssfv 6759 |
. . . . . . . 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 3916 |
. . . . . . . . . . . . . . 15
⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})) |
347 | 330 | eleq2d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (ℎ‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom
(ℎ‘suc 𝑘))) |
348 | 330 | eleq1d 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (ℎ‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘suc 𝑘) ∈ ω)) |
349 | 347, 348 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (ℎ‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom
(ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))) |
350 | 329, 349 | elab 3602 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom
(ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)) |
351 | 346, 350 | syl6ib 254 |
. . . . . . . . . . . . . 14
⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))) |
352 | 351 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))) |
353 | 297, 352 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (∅ ∈ dom
(ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)) |
354 | 353 | simprd 499 |
. . . . . . . . . . 11
⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → dom (ℎ‘suc 𝑘) ∈ ω) |
355 | | nnord 7673 |
. . . . . . . . . . 11
⊢ (dom
(ℎ‘suc 𝑘) ∈ ω → Ord dom
(ℎ‘suc 𝑘)) |
356 | | ordtr 6247 |
. . . . . . . . . . 11
⊢ (Ord dom
(ℎ‘suc 𝑘) → Tr dom (ℎ‘suc 𝑘)) |
357 | | trsuc 6317 |
. . . . . . . . . . . 12
⊢ ((Tr dom
(ℎ‘suc 𝑘) ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → 𝑘 ∈ dom (ℎ‘suc 𝑘)) |
358 | 357 | ex 416 |
. . . . . . . . . . 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 6759 |
. . . . . . . 8
⊢ ((Fun
∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran
ℎ ∧ 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
363 | 340, 343,
361, 362 | syl3anc 1373 |
. . . . . . 7
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
364 | | simpl 486 |
. . . . . . . 8
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran
ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘)) |
365 | | simpr 488 |
. . . . . . . . 9
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) |
366 | 365 | fveq2d 6742 |
. . . . . . . 8
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (𝐹‘(∪ ran
ℎ‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘))) |
367 | 364, 366 | eleq12d 2834 |
. . . . . . 7
⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran
ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → ((∪ ran
ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
368 | 345, 363,
367 | syl2anc 587 |
. . . . . 6
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))) |
369 | 339, 368 | mpbird 260 |
. . . . 5
⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))) |
370 | 369 | ex 416 |
. . . 4
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑘 ∈ ω → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)))) |
371 | 293, 370 | ralrimi 3140 |
. . 3
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑘 ∈ ω (∪
ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))) |
372 | | vex 3427 |
. . . . . 6
⊢ ℎ ∈ V |
373 | 372 | rnex 7711 |
. . . . 5
⊢ ran ℎ ∈ V |
374 | 373 | uniex 7550 |
. . . 4
⊢ ∪ ran ℎ
∈ V |
375 | | feq1 6547 |
. . . . 5
⊢ (𝑔 = ∪
ran ℎ → (𝑔:ω⟶𝐴 ↔ ∪ ran ℎ:ω⟶𝐴)) |
376 | | fveq1 6737 |
. . . . . 6
⊢ (𝑔 = ∪
ran ℎ → (𝑔‘∅) = (∪ ran ℎ‘∅)) |
377 | 376 | eqeq1d 2741 |
. . . . 5
⊢ (𝑔 = ∪
ran ℎ → ((𝑔‘∅) = 𝐶 ↔ (∪ ran ℎ‘∅) = 𝐶)) |
378 | | fveq1 6737 |
. . . . . . 7
⊢ (𝑔 = ∪
ran ℎ → (𝑔‘suc 𝑘) = (∪ ran ℎ‘suc 𝑘)) |
379 | | fveq1 6737 |
. . . . . . . 8
⊢ (𝑔 = ∪
ran ℎ → (𝑔‘𝑘) = (∪ ran ℎ‘𝑘)) |
380 | 379 | fveq2d 6742 |
. . . . . . 7
⊢ (𝑔 = ∪
ran ℎ → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(∪ ran
ℎ‘𝑘))) |
381 | 378, 380 | eleq12d 2834 |
. . . . . 6
⊢ (𝑔 = ∪
ran ℎ → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (∪ ran
ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)))) |
382 | 381 | ralbidv 3121 |
. . . . 5
⊢ (𝑔 = ∪
ran ℎ → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (∪
ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘)))) |
383 | 375, 377,
382 | 3anbi123d 1438 |
. . . 4
⊢ (𝑔 = ∪
ran ℎ → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (∪ ran
ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪
ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))))) |
384 | 374, 383 | spcev 3536 |
. . 3
⊢ ((∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran
ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran
ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
385 | 268, 290,
371, 384 | syl3anc 1373 |
. 2
⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
386 | 385 | exlimiv 1938 |
1
⊢
(∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |