Step | Hyp | Ref
| Expression |
1 | | peano2 7668 |
. . . . . . . 8
⊢ (𝑑 ∈ ω → suc 𝑑 ∈
ω) |
2 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ ran (𝑌‘suc 𝑑) = ∪ ran (𝑌‘suc 𝑑) |
3 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑏 = suc 𝑑 → (𝑌‘𝑏) = (𝑌‘suc 𝑑)) |
4 | 3 | rneqd 5807 |
. . . . . . . . . . . 12
⊢ (𝑏 = suc 𝑑 → ran (𝑌‘𝑏) = ran (𝑌‘suc 𝑑)) |
5 | 4 | unieqd 4833 |
. . . . . . . . . . 11
⊢ (𝑏 = suc 𝑑 → ∪ ran
(𝑌‘𝑏) = ∪ ran (𝑌‘suc 𝑑)) |
6 | 5 | rspceeqv 3552 |
. . . . . . . . . 10
⊢ ((suc
𝑑 ∈ ω ∧
∪ ran (𝑌‘suc 𝑑) = ∪ ran (𝑌‘suc 𝑑)) → ∃𝑏 ∈ ω ∪
ran (𝑌‘suc 𝑑) = ∪
ran (𝑌‘𝑏)) |
7 | 2, 6 | mpan2 691 |
. . . . . . . . 9
⊢ (suc
𝑑 ∈ ω →
∃𝑏 ∈ ω
∪ ran (𝑌‘suc 𝑑) = ∪ ran (𝑌‘𝑏)) |
8 | | fvex 6730 |
. . . . . . . . . . . 12
⊢ (𝑌‘suc 𝑑) ∈ V |
9 | 8 | rnex 7690 |
. . . . . . . . . . 11
⊢ ran
(𝑌‘suc 𝑑) ∈ V |
10 | 9 | uniex 7529 |
. . . . . . . . . 10
⊢ ∪ ran (𝑌‘suc 𝑑) ∈ V |
11 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) |
12 | 11 | elrnmpt 5825 |
. . . . . . . . . 10
⊢ (∪ ran (𝑌‘suc 𝑑) ∈ V → (∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ↔ ∃𝑏 ∈ ω ∪
ran (𝑌‘suc 𝑑) = ∪
ran (𝑌‘𝑏))) |
13 | 10, 12 | ax-mp 5 |
. . . . . . . . 9
⊢ (∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ↔ ∃𝑏 ∈ ω ∪
ran (𝑌‘suc 𝑑) = ∪
ran (𝑌‘𝑏)) |
14 | 7, 13 | sylibr 237 |
. . . . . . . 8
⊢ (suc
𝑑 ∈ ω →
∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |
15 | 1, 14 | syl 17 |
. . . . . . 7
⊢ (𝑑 ∈ ω → ∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |
16 | 15 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |
17 | | intss1 4874 |
. . . . . 6
⊢ (∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) → ∩ ran
(𝑏 ∈ ω ↦
∪ ran (𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘suc 𝑑)) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘suc 𝑑)) |
19 | | fin23lem33.f |
. . . . . 6
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
20 | | fin23lem.f |
. . . . . 6
⊢ (𝜑 → ℎ:ω–1-1→V) |
21 | | fin23lem.g |
. . . . . 6
⊢ (𝜑 → ∪ ran ℎ
⊆ 𝐺) |
22 | | fin23lem.h |
. . . . . 6
⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗))) |
23 | | fin23lem.i |
. . . . . 6
⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) |
24 | 19, 20, 21, 22, 23 | fin23lem35 9961 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∪ ran (𝑌‘suc 𝑑) ⊊ ∪ ran
(𝑌‘𝑑)) |
25 | 18, 24 | sspsstrd 4023 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑑)) |
26 | | dfpss2 4000 |
. . . . 5
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑑) ↔ (∩ ran
(𝑏 ∈ ω ↦
∪ ran (𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘𝑑) ∧ ¬ ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑))) |
27 | 26 | simprbi 500 |
. . . 4
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑑) → ¬ ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
28 | 25, 27 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ¬ ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
29 | 28 | nrexdv 3189 |
. 2
⊢ (𝜑 → ¬ ∃𝑑 ∈ ω ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
30 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑏 = 𝑑 → (𝑌‘𝑏) = (𝑌‘𝑑)) |
31 | 30 | rneqd 5807 |
. . . . . 6
⊢ (𝑏 = 𝑑 → ran (𝑌‘𝑏) = ran (𝑌‘𝑑)) |
32 | 31 | unieqd 4833 |
. . . . 5
⊢ (𝑏 = 𝑑 → ∪ ran
(𝑌‘𝑏) = ∪ ran (𝑌‘𝑑)) |
33 | 32 | cbvmptv 5158 |
. . . 4
⊢ (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = (𝑑 ∈ ω ↦ ∪ ran (𝑌‘𝑑)) |
34 | 33 | elrnmpt 5825 |
. . 3
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) → (∩ ran
(𝑏 ∈ ω ↦
∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ↔ ∃𝑑 ∈ ω ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑))) |
35 | 34 | ibi 270 |
. 2
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) → ∃𝑑 ∈ ω ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
36 | 29, 35 | nsyl 142 |
1
⊢ (𝜑 → ¬ ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |