Metamath Proof Explorer


Theorem elmade2

Description: Membership in the made function in terms of the old function. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion elmade2 ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) )

Proof

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 𝑟 ) = 𝑋 ) ) )