Step |
Hyp |
Ref |
Expression |
1 |
|
elmade |
⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) ) |
2 |
|
oldval |
⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) ) |
3 |
2
|
pweqd |
⊢ ( 𝐴 ∈ On → 𝒫 ( O ‘ 𝐴 ) = 𝒫 ∪ ( M “ 𝐴 ) ) |
4 |
3
|
rexeqdv |
⊢ ( 𝐴 ∈ On → ( ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ↔ ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) ) |
5 |
3 4
|
rexeqbidv |
⊢ ( 𝐴 ∈ On → ( ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ↔ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) ) |
6 |
1 5
|
bitr4d |
⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) ) |