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 10386 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺)) |
| 7 | | fvex 6919 |
. . . . . . 7
⊢ (𝑌‘𝐴) ∈ V |
| 8 | | f1eq1 6799 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → (𝑗:ω–1-1→V ↔ (𝑌‘𝐴):ω–1-1→V)) |
| 9 | | rneq 5947 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑌‘𝐴) → ran 𝑗 = ran (𝑌‘𝐴)) |
| 10 | 9 | unieqd 4920 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑌‘𝐴) → ∪ ran
𝑗 = ∪ ran (𝑌‘𝐴)) |
| 11 | 10 | sseq1d 4015 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → (∪ ran
𝑗 ⊆ 𝐺 ↔ ∪ ran
(𝑌‘𝐴) ⊆ 𝐺)) |
| 12 | 8, 11 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑗 = (𝑌‘𝐴) → ((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) ↔ ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺))) |
| 13 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑌‘𝐴) → (𝑖‘𝑗) = (𝑖‘(𝑌‘𝐴))) |
| 14 | | f1eq1 6799 |
. . . . . . . . . 10
⊢ ((𝑖‘𝑗) = (𝑖‘(𝑌‘𝐴)) → ((𝑖‘𝑗):ω–1-1→V ↔ (𝑖‘(𝑌‘𝐴)):ω–1-1→V)) |
| 15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → ((𝑖‘𝑗):ω–1-1→V ↔ (𝑖‘(𝑌‘𝐴)):ω–1-1→V)) |
| 16 | 13 | rneqd 5949 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑌‘𝐴) → ran (𝑖‘𝑗) = ran (𝑖‘(𝑌‘𝐴))) |
| 17 | 16 | unieqd 4920 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑌‘𝐴) → ∪ ran
(𝑖‘𝑗) = ∪ ran (𝑖‘(𝑌‘𝐴))) |
| 18 | 17, 10 | psseq12d 4097 |
. . . . . . . . 9
⊢ (𝑗 = (𝑌‘𝐴) → (∪ ran
(𝑖‘𝑗) ⊊ ∪ ran
𝑗 ↔ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))) |
| 19 | 15, 18 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑗 = (𝑌‘𝐴) → (((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗) ↔ ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)))) |
| 20 | 12, 19 | imbi12d 344 |
. . . . . . 7
⊢ (𝑗 = (𝑌‘𝐴) → (((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗)) ↔ (((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))))) |
| 21 | 7, 20 | spcv 3605 |
. . . . . 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 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)))) |
| 24 | 6, 23 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑖‘(𝑌‘𝐴)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))) |
| 25 | 24 | simprd 495 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴)) |
| 26 | | frsuc 8477 |
. . . . . . 7
⊢ (𝐴 ∈ ω →
((rec(𝑖, ℎ) ↾ ω)‘suc 𝐴) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝐴))) |
| 27 | 26 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((rec(𝑖, ℎ) ↾ ω)‘suc 𝐴) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝐴))) |
| 28 | 5 | fveq1i 6907 |
. . . . . 6
⊢ (𝑌‘suc 𝐴) = ((rec(𝑖, ℎ) ↾ ω)‘suc 𝐴) |
| 29 | 5 | fveq1i 6907 |
. . . . . . 7
⊢ (𝑌‘𝐴) = ((rec(𝑖, ℎ) ↾ ω)‘𝐴) |
| 30 | 29 | fveq2i 6909 |
. . . . . 6
⊢ (𝑖‘(𝑌‘𝐴)) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝐴)) |
| 31 | 27, 28, 30 | 3eqtr4g 2802 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝑌‘suc 𝐴) = (𝑖‘(𝑌‘𝐴))) |
| 32 | 31 | rneqd 5949 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ran (𝑌‘suc 𝐴) = ran (𝑖‘(𝑌‘𝐴))) |
| 33 | 32 | unieqd 4920 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑌‘suc 𝐴) = ∪ ran (𝑖‘(𝑌‘𝐴))) |
| 34 | 33 | psseq1d 4095 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (∪ ran (𝑌‘suc 𝐴) ⊊ ∪ ran
(𝑌‘𝐴) ↔ ∪ ran
(𝑖‘(𝑌‘𝐴)) ⊊ ∪ ran
(𝑌‘𝐴))) |
| 35 | 25, 34 | mpbird 257 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑌‘suc 𝐴) ⊊ ∪ ran
(𝑌‘𝐴)) |