Step | Hyp | Ref
| Expression |
1 | | peano2 6978 |
. . . . . . . 8
⊢ (𝑑 ∈ ω → suc 𝑑 ∈
ω) |
2 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ ran (𝑌‘suc 𝑑) = ∪ ran (𝑌‘suc 𝑑) |
3 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = suc 𝑑 → (𝑌‘𝑏) = (𝑌‘suc 𝑑)) |
4 | 3 | rneqd 5274 |
. . . . . . . . . . . . 13
⊢ (𝑏 = suc 𝑑 → ran (𝑌‘𝑏) = ran (𝑌‘suc 𝑑)) |
5 | 4 | unieqd 4382 |
. . . . . . . . . . . 12
⊢ (𝑏 = suc 𝑑 → ∪ ran
(𝑌‘𝑏) = ∪ ran (𝑌‘suc 𝑑)) |
6 | 5 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑏 = suc 𝑑 → (∪ ran
(𝑌‘suc 𝑑) = ∪
ran (𝑌‘𝑏) ↔ ∪ ran (𝑌‘suc 𝑑) = ∪ ran (𝑌‘suc 𝑑))) |
7 | 6 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((suc
𝑑 ∈ ω ∧
∪ ran (𝑌‘suc 𝑑) = ∪ ran (𝑌‘suc 𝑑)) → ∃𝑏 ∈ ω ∪
ran (𝑌‘suc 𝑑) = ∪
ran (𝑌‘𝑏)) |
8 | 2, 7 | mpan2 703 |
. . . . . . . . 9
⊢ (suc
𝑑 ∈ ω →
∃𝑏 ∈ ω
∪ ran (𝑌‘suc 𝑑) = ∪ ran (𝑌‘𝑏)) |
9 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑌‘suc 𝑑) ∈ V |
10 | 9 | rnex 6992 |
. . . . . . . . . . 11
⊢ ran
(𝑌‘suc 𝑑) ∈ V |
11 | 10 | uniex 6851 |
. . . . . . . . . 10
⊢ ∪ ran (𝑌‘suc 𝑑) ∈ V |
12 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) |
13 | 12 | elrnmpt 5293 |
. . . . . . . . . 10
⊢ (∪ ran (𝑌‘suc 𝑑) ∈ V → (∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ↔ ∃𝑏 ∈ ω ∪
ran (𝑌‘suc 𝑑) = ∪
ran (𝑌‘𝑏))) |
14 | 11, 13 | ax-mp 5 |
. . . . . . . . 9
⊢ (∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ↔ ∃𝑏 ∈ ω ∪
ran (𝑌‘suc 𝑑) = ∪
ran (𝑌‘𝑏)) |
15 | 8, 14 | sylibr 223 |
. . . . . . . 8
⊢ (suc
𝑑 ∈ ω →
∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |
16 | 1, 15 | syl 17 |
. . . . . . 7
⊢ (𝑑 ∈ ω → ∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |
17 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |
18 | | intss1 4427 |
. . . . . 6
⊢ (∪ ran (𝑌‘suc 𝑑) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) → ∩ ran
(𝑏 ∈ ω ↦
∪ ran (𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘suc 𝑑)) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘suc 𝑑)) |
20 | | fin23lem33.f |
. . . . . 6
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
21 | | fin23lem.f |
. . . . . 6
⊢ (𝜑 → ℎ:ω–1-1→V) |
22 | | fin23lem.g |
. . . . . 6
⊢ (𝜑 → ∪ ran ℎ
⊆ 𝐺) |
23 | | fin23lem.h |
. . . . . 6
⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗))) |
24 | | fin23lem.i |
. . . . . 6
⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) |
25 | 20, 21, 22, 23, 24 | fin23lem35 9052 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∪ ran (𝑌‘suc 𝑑) ⊊ ∪ ran
(𝑌‘𝑑)) |
26 | 19, 25 | sspsstrd 3677 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑑)) |
27 | | dfpss2 3654 |
. . . . 5
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑑) ↔ (∩ ran
(𝑏 ∈ ω ↦
∪ ran (𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘𝑑) ∧ ¬ ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑))) |
28 | 27 | simprbi 479 |
. . . 4
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑑) → ¬ ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
29 | 26, 28 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → ¬ ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
30 | 29 | nrexdv 2984 |
. 2
⊢ (𝜑 → ¬ ∃𝑑 ∈ ω ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
31 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑏 = 𝑑 → (𝑌‘𝑏) = (𝑌‘𝑑)) |
32 | 31 | rneqd 5274 |
. . . . . 6
⊢ (𝑏 = 𝑑 → ran (𝑌‘𝑏) = ran (𝑌‘𝑑)) |
33 | 32 | unieqd 4382 |
. . . . 5
⊢ (𝑏 = 𝑑 → ∪ ran
(𝑌‘𝑏) = ∪ ran (𝑌‘𝑑)) |
34 | 33 | cbvmptv 4678 |
. . . 4
⊢ (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) = (𝑑 ∈ ω ↦ ∪ ran (𝑌‘𝑑)) |
35 | 34 | elrnmpt 5293 |
. . 3
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) → (∩ ran
(𝑏 ∈ ω ↦
∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ↔ ∃𝑑 ∈ ω ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑))) |
36 | 35 | ibi 255 |
. 2
⊢ (∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) → ∃𝑑 ∈ ω ∩
ran (𝑏 ∈ ω
↦ ∪ ran (𝑌‘𝑏)) = ∪ ran (𝑌‘𝑑)) |
37 | 30, 36 | nsyl 134 |
1
⊢ (𝜑 → ¬ ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) |