Proof of Theorem fin23lem35
Step | Hyp | Ref
| Expression |
1 | | fin23lem33.f |
. . . . 5
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
2 | | fin23lem.f |
. . . . 5
⊢ (𝜑 → ℎ:ω–1-1→V) |
3 | | fin23lem.g |
. . . . 5
⊢ (𝜑 → ∪ ran ℎ
⊆ 𝐺) |
4 | | fin23lem.h |
. . . . 5
⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗))) |
5 | | fin23lem.i |
. . . . 5
⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) |
6 | 1, 2, 3, 4, 5 | fin23lem34 9960 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺)) |
7 | | fvex 6730 |
. . . . . . 7
⊢ (𝑌‘𝐴) ∈ V |
8 | | f1eq1 6610 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → (𝑗:ω–1-1→V ↔ (𝑌‘𝐴):ω–1-1→V)) |
9 | | rneq 5805 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑌‘𝐴) → ran 𝑗 = ran (𝑌‘𝐴)) |
10 | 9 | unieqd 4833 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑌‘𝐴) → ∪ ran
𝑗 = ∪ ran (𝑌‘𝐴)) |
11 | 10 | sseq1d 3932 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → (∪ ran
𝑗 ⊆ 𝐺 ↔ ∪ ran
(𝑌‘𝐴) ⊆ 𝐺)) |
12 | 8, 11 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑗 = (𝑌‘𝐴) → ((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) ↔ ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺))) |
13 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑌‘𝐴) → (𝑖‘𝑗) = (𝑖‘(𝑌‘𝐴))) |
14 | | f1eq1 6610 |
. . . . . . . . . 10
⊢ ((𝑖‘𝑗) = (𝑖‘(𝑌‘𝐴)) → ((𝑖‘𝑗):ω–1-1→V ↔ (𝑖‘(𝑌‘𝐴)):ω–1-1→V)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → ((𝑖‘𝑗):ω–1-1→V ↔ (𝑖‘(𝑌‘𝐴)):ω–1-1→V)) |
16 | 13 | rneqd 5807 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑌‘𝐴) → ran (𝑖‘𝑗) = ran (𝑖‘(𝑌‘𝐴))) |
17 | 16 | unieqd 4833 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑌‘𝐴) → ∪ ran
(𝑖‘𝑗) = ∪ ran (𝑖‘(𝑌‘𝐴))) |
18 | 17, 10 | psseq12d 4009 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → (∪ ran
(𝑖‘𝑗) ⊊ ∪ ran
𝑗 ↔ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))) |
19 | 15, 18 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑗 = (𝑌‘𝐴) → (((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗) ↔ ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)))) |
20 | 12, 19 | imbi12d 348 |
. . . . . . 7
⊢ (𝑗 = (𝑌‘𝐴) → (((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗)) ↔ (((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))))) |
21 | 7, 20 | spcv 3520 |
. . . . . 6
⊢
(∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗)) → (((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)))) |
22 | 4, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → (((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)))) |
23 | 22 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)))) |
24 | 6, 23 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))) |
25 | 24 | simprd 499 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)) |
26 | | frsuc 8172 |
. . . . . . 7
⊢ (𝐴 ∈ ω →
((rec(𝑖, ℎ) ↾ ω)‘suc 𝐴) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝐴))) |
27 | 26 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((rec(𝑖, ℎ) ↾ ω)‘suc 𝐴) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝐴))) |
28 | 5 | fveq1i 6718 |
. . . . . 6
⊢ (𝑌‘suc 𝐴) = ((rec(𝑖, ℎ) ↾ ω)‘suc 𝐴) |
29 | 5 | fveq1i 6718 |
. . . . . . 7
⊢ (𝑌‘𝐴) = ((rec(𝑖, ℎ) ↾ ω)‘𝐴) |
30 | 29 | fveq2i 6720 |
. . . . . 6
⊢ (𝑖‘(𝑌‘𝐴)) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝐴)) |
31 | 27, 28, 30 | 3eqtr4g 2803 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝑌‘suc 𝐴) = (𝑖‘(𝑌‘𝐴))) |
32 | 31 | rneqd 5807 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ran (𝑌‘suc 𝐴) = ran (𝑖‘(𝑌‘𝐴))) |
33 | 32 | unieqd 4833 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑌‘suc 𝐴) = ∪ ran (𝑖‘(𝑌‘𝐴))) |
34 | 33 | psseq1d 4007 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (∪ ran (𝑌‘suc 𝐴) ⊊ ∪ ran
(𝑌‘𝐴) ↔ ∪ ran
(𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))) |
35 | 25, 34 | mpbird 260 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑌‘suc 𝐴) ⊊ ∪ ran
(𝑌‘𝐴)) |