| Step | Hyp | Ref
| Expression |
| 1 | | fin23lem.a |
. . . 4
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) |
| 2 | 1 | fin23lem13 10372 |
. . 3
⊢ (𝑐 ∈ ω → (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐)) |
| 3 | 2 | rgen 3063 |
. 2
⊢
∀𝑐 ∈
ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐) |
| 4 | | fveq1 6905 |
. . . . . 6
⊢ (𝑏 = 𝑈 → (𝑏‘suc 𝑐) = (𝑈‘suc 𝑐)) |
| 5 | | fveq1 6905 |
. . . . . 6
⊢ (𝑏 = 𝑈 → (𝑏‘𝑐) = (𝑈‘𝑐)) |
| 6 | 4, 5 | sseq12d 4017 |
. . . . 5
⊢ (𝑏 = 𝑈 → ((𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) ↔ (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐))) |
| 7 | 6 | ralbidv 3178 |
. . . 4
⊢ (𝑏 = 𝑈 → (∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) ↔ ∀𝑐 ∈ ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐))) |
| 8 | | rneq 5947 |
. . . . . 6
⊢ (𝑏 = 𝑈 → ran 𝑏 = ran 𝑈) |
| 9 | 8 | inteqd 4951 |
. . . . 5
⊢ (𝑏 = 𝑈 → ∩ ran
𝑏 = ∩ ran 𝑈) |
| 10 | 9, 8 | eleq12d 2835 |
. . . 4
⊢ (𝑏 = 𝑈 → (∩ ran
𝑏 ∈ ran 𝑏 ↔ ∩ ran 𝑈 ∈ ran 𝑈)) |
| 11 | 7, 10 | imbi12d 344 |
. . 3
⊢ (𝑏 = 𝑈 → ((∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏) ↔ (∀𝑐 ∈ ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐) → ∩ ran
𝑈 ∈ ran 𝑈))) |
| 12 | | fin23lem17.f |
. . . . . 6
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
| 13 | 12 | isfin3ds 10369 |
. . . . 5
⊢ (∪ ran 𝑡 ∈ 𝐹 → (∪ ran
𝑡 ∈ 𝐹 ↔ ∀𝑏 ∈ (𝒫 ∪ ran 𝑡 ↑m ω)(∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏))) |
| 14 | 13 | ibi 267 |
. . . 4
⊢ (∪ ran 𝑡 ∈ 𝐹 → ∀𝑏 ∈ (𝒫 ∪ ran 𝑡 ↑m ω)(∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏)) |
| 15 | 14 | adantr 480 |
. . 3
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∀𝑏 ∈ (𝒫 ∪ ran 𝑡 ↑m ω)(∀𝑐 ∈ ω (𝑏‘suc 𝑐) ⊆ (𝑏‘𝑐) → ∩ ran
𝑏 ∈ ran 𝑏)) |
| 16 | 1 | fnseqom 8495 |
. . . . . 6
⊢ 𝑈 Fn ω |
| 17 | | dffn3 6748 |
. . . . . 6
⊢ (𝑈 Fn ω ↔ 𝑈:ω⟶ran 𝑈) |
| 18 | 16, 17 | mpbi 230 |
. . . . 5
⊢ 𝑈:ω⟶ran 𝑈 |
| 19 | | pwuni 4945 |
. . . . . 6
⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑈 |
| 20 | 1 | fin23lem16 10375 |
. . . . . . 7
⊢ ∪ ran 𝑈 = ∪ ran 𝑡 |
| 21 | 20 | pweqi 4616 |
. . . . . 6
⊢ 𝒫
∪ ran 𝑈 = 𝒫 ∪
ran 𝑡 |
| 22 | 19, 21 | sseqtri 4032 |
. . . . 5
⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡 |
| 23 | | fss 6752 |
. . . . 5
⊢ ((𝑈:ω⟶ran 𝑈 ∧ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡) → 𝑈:ω⟶𝒫 ∪ ran 𝑡) |
| 24 | 18, 22, 23 | mp2an 692 |
. . . 4
⊢ 𝑈:ω⟶𝒫 ∪ ran 𝑡 |
| 25 | | vex 3484 |
. . . . . . . 8
⊢ 𝑡 ∈ V |
| 26 | 25 | rnex 7932 |
. . . . . . 7
⊢ ran 𝑡 ∈ V |
| 27 | 26 | uniex 7761 |
. . . . . 6
⊢ ∪ ran 𝑡 ∈ V |
| 28 | 27 | pwex 5380 |
. . . . 5
⊢ 𝒫
∪ ran 𝑡 ∈ V |
| 29 | | f1f 6804 |
. . . . . . 7
⊢ (𝑡:ω–1-1→𝑉 → 𝑡:ω⟶𝑉) |
| 30 | | dmfex 7927 |
. . . . . . 7
⊢ ((𝑡 ∈ V ∧ 𝑡:ω⟶𝑉) → ω ∈
V) |
| 31 | 25, 29, 30 | sylancr 587 |
. . . . . 6
⊢ (𝑡:ω–1-1→𝑉 → ω ∈ V) |
| 32 | 31 | adantl 481 |
. . . . 5
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ω ∈ V) |
| 33 | | elmapg 8879 |
. . . . 5
⊢
((𝒫 ∪ ran 𝑡 ∈ V ∧ ω ∈ V) →
(𝑈 ∈ (𝒫 ∪ ran 𝑡 ↑m ω) ↔ 𝑈:ω⟶𝒫 ∪ ran 𝑡)) |
| 34 | 28, 32, 33 | sylancr 587 |
. . . 4
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → (𝑈 ∈ (𝒫 ∪ ran 𝑡 ↑m ω) ↔ 𝑈:ω⟶𝒫 ∪ ran 𝑡)) |
| 35 | 24, 34 | mpbiri 258 |
. . 3
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → 𝑈 ∈ (𝒫 ∪ ran 𝑡 ↑m
ω)) |
| 36 | 11, 15, 35 | rspcdva 3623 |
. 2
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → (∀𝑐 ∈ ω (𝑈‘suc 𝑐) ⊆ (𝑈‘𝑐) → ∩ ran
𝑈 ∈ ran 𝑈)) |
| 37 | 3, 36 | mpi 20 |
1
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∩ ran
𝑈 ∈ ran 𝑈) |