Metamath Proof Explorer

Theorem elmade

Description: Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 madef ⊢ M : On ⟶ 𝒫 No
2 1 ffvelrni ⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) ∈ 𝒫 No )
3 2 elpwid ⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) ⊆ No )
4 3 sseld ⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) → 𝑋 ∈ No ) )
5 scutcl ⊢ ( 𝑙 <<s 𝑟 → ( 𝑙 |s 𝑟 ) ∈ No )
6 eleq1 ⊢ ( ( 𝑙 |s 𝑟 ) = 𝑋 → ( ( 𝑙 |s 𝑟 ) ∈ No ↔ 𝑋 ∈ No ) )
7 6 biimpd ⊢ ( ( 𝑙 |s 𝑟 ) = 𝑋 → ( ( 𝑙 |s 𝑟 ) ∈ No → 𝑋 ∈ No ) )
8 5 7 mpan9 ⊢ ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) → 𝑋 ∈ No )
9 8 rexlimivw ⊢ ( ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) → 𝑋 ∈ No )
10 9 rexlimivw ⊢ ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) → 𝑋 ∈ No )
11 10 a1i ⊢ ( 𝐴 ∈ On → ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) → 𝑋 ∈ No ) )
12 madeval2 ⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } )
13 12 eleq2d ⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ 𝑋 ∈ { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } ) )
14 eqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝑙 |s 𝑟 ) = 𝑥 ↔ ( 𝑙 |s 𝑟 ) = 𝑋 ) )
15 14 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) )
16 15 2rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) )
17 16 elrab3 ⊢ ( 𝑋 ∈ No → ( 𝑋 ∈ { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } ↔ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) )
18 13 17 sylan9bb ⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) )
19 18 ex ⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ No → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) ) )
20 4 11 19 pm5.21ndd ⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑋 ) ) )