Step | Hyp | Ref
| Expression |
1 | | fin23lem.a |
. . . 4
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) |
2 | 1 | fin23lem13 9959 |
. . 3
⊢ (𝑐 ∈ ω → (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐)) |
3 | 2 | rgen 3072 |
. 2
⊢
∀𝑐 ∈
ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐) |
4 | | fveq1 6725 |
. . . . . 6
⊢ (𝑏 = 𝑈 → (𝑏‘suc 𝑐) = (𝑈‘suc 𝑐)) |
5 | | fveq1 6725 |
. . . . . 6
⊢ (𝑏 = 𝑈 → (𝑏‘𝑐) = (𝑈‘𝑐)) |
6 | 4, 5 | sseq12d 3943 |
. . . . 5
⊢ (𝑏 = 𝑈 → ((𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) ↔ (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐))) |
7 | 6 | ralbidv 3119 |
. . . 4
⊢ (𝑏 = 𝑈 → (∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) ↔ ∀𝑐 ∈ ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐))) |
8 | | rneq 5814 |
. . . . . 6
⊢ (𝑏 = 𝑈 → ran 𝑏 = ran 𝑈) |
9 | 8 | inteqd 4873 |
. . . . 5
⊢ (𝑏 = 𝑈 → ∩ ran
𝑏 = ∩ ran 𝑈) |
10 | 9, 8 | eleq12d 2833 |
. . . 4
⊢ (𝑏 = 𝑈 → (∩ ran
𝑏 ∈ ran 𝑏 ↔ ∩ ran 𝑈 ∈ ran 𝑈)) |
11 | 7, 10 | imbi12d 348 |
. . 3
⊢ (𝑏 = 𝑈 → ((∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏) ↔ (∀𝑐 ∈ ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐) → ∩ ran
𝑈 ∈ ran 𝑈))) |
12 | | fin23lem17.f |
. . . . . 6
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
13 | 12 | isfin3ds 9956 |
. . . . 5
⊢ (∪ ran 𝑡 ∈ 𝐹 → (∪ ran
𝑡 ∈ 𝐹 ↔ ∀𝑏 ∈ (𝒫 ∪ ran 𝑡 ↑m ω)(∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏))) |
14 | 13 | ibi 270 |
. . . 4
⊢ (∪ ran 𝑡 ∈ 𝐹 → ∀𝑏 ∈ (𝒫 ∪ ran 𝑡 ↑m ω)(∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏)) |
15 | 14 | adantr 484 |
. . 3
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∀𝑏 ∈ (𝒫 ∪ ran 𝑡 ↑m ω)(∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏)) |
16 | 1 | fnseqom 8200 |
. . . . . 6
⊢ 𝑈 Fn ω |
17 | | dffn3 6567 |
. . . . . 6
⊢ (𝑈 Fn ω ↔ 𝑈:ω⟶ran 𝑈) |
18 | 16, 17 | mpbi 233 |
. . . . 5
⊢ 𝑈:ω⟶ran 𝑈 |
19 | | pwuni 4867 |
. . . . . 6
⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑈 |
20 | 1 | fin23lem16 9962 |
. . . . . . 7
⊢ ∪ ran 𝑈 = ∪ ran 𝑡 |
21 | 20 | pweqi 4540 |
. . . . . 6
⊢ 𝒫
∪ ran 𝑈 = 𝒫 ∪
ran 𝑡 |
22 | 19, 21 | sseqtri 3946 |
. . . . 5
⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡 |
23 | | fss 6571 |
. . . . 5
⊢ ((𝑈:ω⟶ran 𝑈 ∧ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡) → 𝑈:ω⟶𝒫 ∪ ran 𝑡) |
24 | 18, 22, 23 | mp2an 692 |
. . . 4
⊢ 𝑈:ω⟶𝒫 ∪ ran 𝑡 |
25 | | vex 3419 |
. . . . . . . 8
⊢ 𝑡 ∈ V |
26 | 25 | rnex 7699 |
. . . . . . 7
⊢ ran 𝑡 ∈ V |
27 | 26 | uniex 7538 |
. . . . . 6
⊢ ∪ ran 𝑡 ∈ V |
28 | 27 | pwex 5282 |
. . . . 5
⊢ 𝒫
∪ ran 𝑡 ∈ V |
29 | | f1f 6624 |
. . . . . . 7
⊢ (𝑡:ω–1-1→𝑉 → 𝑡:ω⟶𝑉) |
30 | | dmfex 7694 |
. . . . . . 7
⊢ ((𝑡 ∈ V ∧ 𝑡:ω⟶𝑉) → ω ∈
V) |
31 | 25, 29, 30 | sylancr 590 |
. . . . . 6
⊢ (𝑡:ω–1-1→𝑉 → ω ∈ V) |
32 | 31 | adantl 485 |
. . . . 5
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ω ∈ V) |
33 | | elmapg 8530 |
. . . . 5
⊢
((𝒫 ∪ ran 𝑡 ∈ V ∧ ω ∈ V) →
(𝑈 ∈ (𝒫 ∪ ran 𝑡 ↑m ω) ↔ 𝑈:ω⟶𝒫 ∪ ran 𝑡)) |
34 | 28, 32, 33 | sylancr 590 |
. . . 4
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → (𝑈 ∈ (𝒫 ∪ ran 𝑡 ↑m ω) ↔ 𝑈:ω⟶𝒫 ∪ ran 𝑡)) |
35 | 24, 34 | mpbiri 261 |
. . 3
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → 𝑈 ∈ (𝒫 ∪ ran 𝑡 ↑m
ω)) |
36 | 11, 15, 35 | rspcdva 3546 |
. 2
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → (∀𝑐 ∈ ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐) → ∩ ran
𝑈 ∈ ran 𝑈)) |
37 | 3, 36 | mpi 20 |
1
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∩ ran
𝑈 ∈ ran 𝑈) |