Metamath Proof Explorer


Theorem elmade

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

Ref Expression
Assertion elmade A On X M A l 𝒫 M A r 𝒫 M A l s r l | s r = X

Proof

Step Hyp Ref Expression
1 madef M : On 𝒫 No
2 1 ffvelrni A On M A 𝒫 No
3 2 elpwid A On M A No
4 3 sseld A On X M A X No
5 scutcl l s r l | s r No
6 eleq1 l | s r = X l | s r No X No
7 6 biimpd l | s r = X l | s r No X No
8 5 7 mpan9 l s r l | s r = X X No
9 8 rexlimivw r 𝒫 M A l s r l | s r = X X No
10 9 rexlimivw l 𝒫 M A r 𝒫 M A l s r l | s r = X X No
11 10 a1i A On l 𝒫 M A r 𝒫 M A l s r l | s r = X X No
12 madeval2 A On M A = x No | l 𝒫 M A r 𝒫 M A l s r l | s r = x
13 12 eleq2d A On X M A X x No | l 𝒫 M A r 𝒫 M A l s r l | s r = x
14 eqeq2 x = X l | s r = x l | s r = X
15 14 anbi2d x = X l s r l | s r = x l s r l | s r = X
16 15 2rexbidv x = X l 𝒫 M A r 𝒫 M A l s r l | s r = x l 𝒫 M A r 𝒫 M A l s r l | s r = X
17 16 elrab3 X No X x No | l 𝒫 M A r 𝒫 M A l s r l | s r = x l 𝒫 M A r 𝒫 M A l s r l | s r = X
18 13 17 sylan9bb A On X No X M A l 𝒫 M A r 𝒫 M A l s r l | s r = X
19 18 ex A On X No X M A l 𝒫 M A r 𝒫 M A l s r l | s r = X
20 4 11 19 pm5.21ndd A On X M A l 𝒫 M A r 𝒫 M A l s r l | s r = X