Step |
Hyp |
Ref |
Expression |
1 |
|
fin23lem.a |
⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 ) |
2 |
|
fin23lem17.f |
⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } |
3 |
1
|
fin23lem13 |
⊢ ( 𝑐 ∈ ω → ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) ) |
4 |
3
|
rgen |
⊢ ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) |
5 |
|
fveq1 |
⊢ ( 𝑏 = 𝑈 → ( 𝑏 ‘ suc 𝑐 ) = ( 𝑈 ‘ suc 𝑐 ) ) |
6 |
|
fveq1 |
⊢ ( 𝑏 = 𝑈 → ( 𝑏 ‘ 𝑐 ) = ( 𝑈 ‘ 𝑐 ) ) |
7 |
5 6
|
sseq12d |
⊢ ( 𝑏 = 𝑈 → ( ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) ↔ ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) ) ) |
8 |
7
|
ralbidv |
⊢ ( 𝑏 = 𝑈 → ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) ↔ ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) ) ) |
9 |
|
rneq |
⊢ ( 𝑏 = 𝑈 → ran 𝑏 = ran 𝑈 ) |
10 |
9
|
inteqd |
⊢ ( 𝑏 = 𝑈 → ∩ ran 𝑏 = ∩ ran 𝑈 ) |
11 |
10 9
|
eleq12d |
⊢ ( 𝑏 = 𝑈 → ( ∩ ran 𝑏 ∈ ran 𝑏 ↔ ∩ ran 𝑈 ∈ ran 𝑈 ) ) |
12 |
8 11
|
imbi12d |
⊢ ( 𝑏 = 𝑈 → ( ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ↔ ( ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) → ∩ ran 𝑈 ∈ ran 𝑈 ) ) ) |
13 |
2
|
isfin3ds |
⊢ ( ∪ ran 𝑡 ∈ 𝐹 → ( ∪ ran 𝑡 ∈ 𝐹 ↔ ∀ 𝑏 ∈ ( 𝒫 ∪ ran 𝑡 ↑m ω ) ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) ) |
14 |
13
|
ibi |
⊢ ( ∪ ran 𝑡 ∈ 𝐹 → ∀ 𝑏 ∈ ( 𝒫 ∪ ran 𝑡 ↑m ω ) ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) |
15 |
14
|
adantr |
⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∀ 𝑏 ∈ ( 𝒫 ∪ ran 𝑡 ↑m ω ) ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) |
16 |
1
|
fnseqom |
⊢ 𝑈 Fn ω |
17 |
|
dffn3 |
⊢ ( 𝑈 Fn ω ↔ 𝑈 : ω ⟶ ran 𝑈 ) |
18 |
16 17
|
mpbi |
⊢ 𝑈 : ω ⟶ ran 𝑈 |
19 |
|
pwuni |
⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑈 |
20 |
1
|
fin23lem16 |
⊢ ∪ ran 𝑈 = ∪ ran 𝑡 |
21 |
20
|
pweqi |
⊢ 𝒫 ∪ ran 𝑈 = 𝒫 ∪ ran 𝑡 |
22 |
19 21
|
sseqtri |
⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡 |
23 |
|
fss |
⊢ ( ( 𝑈 : ω ⟶ ran 𝑈 ∧ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡 ) → 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡 ) |
24 |
18 22 23
|
mp2an |
⊢ 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡 |
25 |
|
vex |
⊢ 𝑡 ∈ V |
26 |
25
|
rnex |
⊢ ran 𝑡 ∈ V |
27 |
26
|
uniex |
⊢ ∪ ran 𝑡 ∈ V |
28 |
27
|
pwex |
⊢ 𝒫 ∪ ran 𝑡 ∈ V |
29 |
|
f1f |
⊢ ( 𝑡 : ω –1-1→ 𝑉 → 𝑡 : ω ⟶ 𝑉 ) |
30 |
|
dmfex |
⊢ ( ( 𝑡 ∈ V ∧ 𝑡 : ω ⟶ 𝑉 ) → ω ∈ V ) |
31 |
25 29 30
|
sylancr |
⊢ ( 𝑡 : ω –1-1→ 𝑉 → ω ∈ V ) |
32 |
31
|
adantl |
⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ω ∈ V ) |
33 |
|
elmapg |
⊢ ( ( 𝒫 ∪ ran 𝑡 ∈ V ∧ ω ∈ V ) → ( 𝑈 ∈ ( 𝒫 ∪ ran 𝑡 ↑m ω ) ↔ 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡 ) ) |
34 |
28 32 33
|
sylancr |
⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ( 𝑈 ∈ ( 𝒫 ∪ ran 𝑡 ↑m ω ) ↔ 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡 ) ) |
35 |
24 34
|
mpbiri |
⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → 𝑈 ∈ ( 𝒫 ∪ ran 𝑡 ↑m ω ) ) |
36 |
12 15 35
|
rspcdva |
⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ( ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) → ∩ ran 𝑈 ∈ ran 𝑈 ) ) |
37 |
4 36
|
mpi |
⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∩ ran 𝑈 ∈ ran 𝑈 ) |