| Step | Hyp | Ref
| Expression |
| 1 | | simprl 771 |
. . . . . . . 8
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → 𝑐 ∈ 𝐴) |
| 2 | | limsuc 7870 |
. . . . . . . . 9
⊢ (Lim
𝐴 → (𝑐 ∈ 𝐴 ↔ suc 𝑐 ∈ 𝐴)) |
| 3 | 2 | ad2antrr 726 |
. . . . . . . 8
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → (𝑐 ∈ 𝐴 ↔ suc 𝑐 ∈ 𝐴)) |
| 4 | 1, 3 | mpbid 232 |
. . . . . . 7
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → suc 𝑐 ∈ 𝐴) |
| 5 | | simprr 773 |
. . . . . . . 8
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → 𝑥 ∈ ( M ‘𝑐)) |
| 6 | | limord 6444 |
. . . . . . . . . . . 12
⊢ (Lim
𝐴 → Ord 𝐴) |
| 7 | | elex 3501 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
| 8 | 6, 7 | anim12i 613 |
. . . . . . . . . . 11
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → (Ord 𝐴 ∧ 𝐴 ∈ V)) |
| 9 | | elon2 6395 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) |
| 10 | 8, 9 | sylibr 234 |
. . . . . . . . . 10
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ On) |
| 11 | | onelon 6409 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ On) |
| 12 | 10, 1, 11 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → 𝑐 ∈ On) |
| 13 | | madeoldsuc 27923 |
. . . . . . . . 9
⊢ (𝑐 ∈ On → ( M
‘𝑐) = ( O ‘suc
𝑐)) |
| 14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → ( M ‘𝑐) = ( O ‘suc 𝑐)) |
| 15 | 5, 14 | eleqtrd 2843 |
. . . . . . 7
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → 𝑥 ∈ ( O ‘suc 𝑐)) |
| 16 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑏 = suc 𝑐 → ( O ‘𝑏) = ( O ‘suc 𝑐)) |
| 17 | 16 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑏 = suc 𝑐 → (𝑥 ∈ ( O ‘𝑏) ↔ 𝑥 ∈ ( O ‘suc 𝑐))) |
| 18 | 17 | rspcev 3622 |
. . . . . . 7
⊢ ((suc
𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘suc 𝑐)) → ∃𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘𝑏)) |
| 19 | 4, 15, 18 | syl2anc 584 |
. . . . . 6
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑐))) → ∃𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘𝑏)) |
| 20 | 19 | rexlimdvaa 3156 |
. . . . 5
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → (∃𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘𝑐) → ∃𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘𝑏))) |
| 21 | | simprl 771 |
. . . . . . 7
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘𝑏))) → 𝑏 ∈ 𝐴) |
| 22 | | oldssmade 27916 |
. . . . . . . 8
⊢ ( O
‘𝑏) ⊆ ( M
‘𝑏) |
| 23 | | simprr 773 |
. . . . . . . 8
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘𝑏))) → 𝑥 ∈ ( O ‘𝑏)) |
| 24 | 22, 23 | sselid 3981 |
. . . . . . 7
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘𝑏))) → 𝑥 ∈ ( M ‘𝑏)) |
| 25 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑐 = 𝑏 → ( M ‘𝑐) = ( M ‘𝑏)) |
| 26 | 25 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑐 = 𝑏 → (𝑥 ∈ ( M ‘𝑐) ↔ 𝑥 ∈ ( M ‘𝑏))) |
| 27 | 26 | rspcev 3622 |
. . . . . . 7
⊢ ((𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘𝑏)) → ∃𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘𝑐)) |
| 28 | 21, 24, 27 | syl2anc 584 |
. . . . . 6
⊢ (((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) ∧ (𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘𝑏))) → ∃𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘𝑐)) |
| 29 | 28 | rexlimdvaa 3156 |
. . . . 5
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → (∃𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘𝑏) → ∃𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘𝑐))) |
| 30 | 20, 29 | impbid 212 |
. . . 4
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → (∃𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘𝑐) ↔ ∃𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘𝑏))) |
| 31 | | elold 27908 |
. . . . 5
⊢ (𝐴 ∈ On → (𝑥 ∈ ( O ‘𝐴) ↔ ∃𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘𝑐))) |
| 32 | 10, 31 | syl 17 |
. . . 4
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ ( O ‘𝐴) ↔ ∃𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘𝑐))) |
| 33 | | eliun 4995 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑏 ∈ 𝐴 ( O ‘𝑏) ↔ ∃𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘𝑏)) |
| 34 | 33 | a1i 11 |
. . . 4
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ ∪
𝑏 ∈ 𝐴 ( O ‘𝑏) ↔ ∃𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘𝑏))) |
| 35 | 30, 32, 34 | 3bitr4d 311 |
. . 3
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ ( O ‘𝐴) ↔ 𝑥 ∈ ∪
𝑏 ∈ 𝐴 ( O ‘𝑏))) |
| 36 | 35 | eqrdv 2735 |
. 2
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪
𝑏 ∈ 𝐴 ( O ‘𝑏)) |
| 37 | | oldf 27896 |
. . 3
⊢ O
:On⟶𝒫 No |
| 38 | | ffun 6739 |
. . 3
⊢ ( O
:On⟶𝒫 No → Fun O
) |
| 39 | | funiunfv 7268 |
. . 3
⊢ (Fun O
→ ∪ 𝑏 ∈ 𝐴 ( O ‘𝑏) = ∪ ( O “
𝐴)) |
| 40 | 37, 38, 39 | mp2b 10 |
. 2
⊢ ∪ 𝑏 ∈ 𝐴 ( O ‘𝑏) = ∪ ( O “
𝐴) |
| 41 | 36, 40 | eqtrdi 2793 |
1
⊢ ((Lim
𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “
𝐴)) |