| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simprl |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑐 ∈ 𝐴 ) |
| 2 |
|
limsuc |
⊢ ( Lim 𝐴 → ( 𝑐 ∈ 𝐴 ↔ suc 𝑐 ∈ 𝐴 ) ) |
| 3 |
2
|
ad2antrr |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → ( 𝑐 ∈ 𝐴 ↔ suc 𝑐 ∈ 𝐴 ) ) |
| 4 |
1 3
|
mpbid |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → suc 𝑐 ∈ 𝐴 ) |
| 5 |
|
simprr |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑥 ∈ ( M ‘ 𝑐 ) ) |
| 6 |
|
limord |
⊢ ( Lim 𝐴 → Ord 𝐴 ) |
| 7 |
|
elex |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) |
| 8 |
6 7
|
anim12i |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( Ord 𝐴 ∧ 𝐴 ∈ V ) ) |
| 9 |
|
elon2 |
⊢ ( 𝐴 ∈ On ↔ ( Ord 𝐴 ∧ 𝐴 ∈ V ) ) |
| 10 |
8 9
|
sylibr |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ On ) |
| 11 |
|
onelon |
⊢ ( ( 𝐴 ∈ On ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ On ) |
| 12 |
10 1 11
|
syl2an2r |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑐 ∈ On ) |
| 13 |
|
madeoldsuc |
⊢ ( 𝑐 ∈ On → ( M ‘ 𝑐 ) = ( O ‘ suc 𝑐 ) ) |
| 14 |
12 13
|
syl |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → ( M ‘ 𝑐 ) = ( O ‘ suc 𝑐 ) ) |
| 15 |
5 14
|
eleqtrd |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑥 ∈ ( O ‘ suc 𝑐 ) ) |
| 16 |
|
fveq2 |
⊢ ( 𝑏 = suc 𝑐 → ( O ‘ 𝑏 ) = ( O ‘ suc 𝑐 ) ) |
| 17 |
16
|
eleq2d |
⊢ ( 𝑏 = suc 𝑐 → ( 𝑥 ∈ ( O ‘ 𝑏 ) ↔ 𝑥 ∈ ( O ‘ suc 𝑐 ) ) ) |
| 18 |
17
|
rspcev |
⊢ ( ( suc 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ suc 𝑐 ) ) → ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) |
| 19 |
4 15 18
|
syl2anc |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) |
| 20 |
19
|
expr |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝐴 ) → ( 𝑥 ∈ ( M ‘ 𝑐 ) → ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) ) |
| 21 |
20
|
rexlimdva |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) → ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) ) |
| 22 |
|
simprl |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → 𝑏 ∈ 𝐴 ) |
| 23 |
|
onelon |
⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ On ) |
| 24 |
10 22 23
|
syl2an2r |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → 𝑏 ∈ On ) |
| 25 |
|
oldssmade |
⊢ ( 𝑏 ∈ On → ( O ‘ 𝑏 ) ⊆ ( M ‘ 𝑏 ) ) |
| 26 |
24 25
|
syl |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → ( O ‘ 𝑏 ) ⊆ ( M ‘ 𝑏 ) ) |
| 27 |
|
simprr |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → 𝑥 ∈ ( O ‘ 𝑏 ) ) |
| 28 |
26 27
|
sseldd |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → 𝑥 ∈ ( M ‘ 𝑏 ) ) |
| 29 |
|
fveq2 |
⊢ ( 𝑐 = 𝑏 → ( M ‘ 𝑐 ) = ( M ‘ 𝑏 ) ) |
| 30 |
29
|
eleq2d |
⊢ ( 𝑐 = 𝑏 → ( 𝑥 ∈ ( M ‘ 𝑐 ) ↔ 𝑥 ∈ ( M ‘ 𝑏 ) ) ) |
| 31 |
30
|
rspcev |
⊢ ( ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑏 ) ) → ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) |
| 32 |
22 28 31
|
syl2anc |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) |
| 33 |
32
|
expr |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝑥 ∈ ( O ‘ 𝑏 ) → ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) ) |
| 34 |
33
|
rexlimdva |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) → ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) ) |
| 35 |
21 34
|
impbid |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) ) |
| 36 |
|
elold |
⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) ) |
| 37 |
10 36
|
syl |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) ) |
| 38 |
|
eliun |
⊢ ( 𝑥 ∈ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) |
| 39 |
38
|
a1i |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) ) |
| 40 |
35 37 39
|
3bitr4d |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ 𝑥 ∈ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) ) ) |
| 41 |
40
|
eqrdv |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( O ‘ 𝐴 ) = ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) ) |
| 42 |
|
oldf |
⊢ O : On ⟶ 𝒫 No |
| 43 |
|
ffun |
⊢ ( O : On ⟶ 𝒫 No → Fun O ) |
| 44 |
|
funiunfv |
⊢ ( Fun O → ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) = ∪ ( O “ 𝐴 ) ) |
| 45 |
42 43 44
|
mp2b |
⊢ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) = ∪ ( O “ 𝐴 ) |
| 46 |
41 45
|
eqtrdi |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( O ‘ 𝐴 ) = ∪ ( O “ 𝐴 ) ) |