Metamath Proof Explorer


Theorem madeval2

Description: Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021)

Ref Expression
Assertion madeval2 AOnMA=xNo|a𝒫MAb𝒫MAasba|sb=x

Proof

Step Hyp Ref Expression
1 madeval AOnMA=|s𝒫MA×𝒫MA
2 scutcl asba|sbNo
3 eleq1 a|sb=xa|sbNoxNo
4 3 biimpd a|sb=xa|sbNoxNo
5 2 4 mpan9 asba|sb=xxNo
6 5 rexlimivw b𝒫MAasba|sb=xxNo
7 6 rexlimivw a𝒫MAb𝒫MAasba|sb=xxNo
8 7 pm4.71ri a𝒫MAb𝒫MAasba|sb=xxNoa𝒫MAb𝒫MAasba|sb=x
9 8 abbii x|a𝒫MAb𝒫MAasba|sb=x=x|xNoa𝒫MAb𝒫MAasba|sb=x
10 eleq1 y=abysabs
11 breq1 y=aby|sxab|sx
12 10 11 anbi12d y=abysy|sxabsab|sx
13 12 rexxp y𝒫MA×𝒫MAysy|sxa𝒫MAb𝒫MAabsab|sx
14 imaindm |s𝒫MA×𝒫MA=|s𝒫MA×𝒫MAdom|s
15 dmscut dom|s=s
16 15 ineq2i 𝒫MA×𝒫MAdom|s=𝒫MA×𝒫MAs
17 16 imaeq2i |s𝒫MA×𝒫MAdom|s=|s𝒫MA×𝒫MAs
18 14 17 eqtri |s𝒫MA×𝒫MA=|s𝒫MA×𝒫MAs
19 18 eleq2i x|s𝒫MA×𝒫MAx|s𝒫MA×𝒫MAs
20 vex xV
21 20 elima x|s𝒫MA×𝒫MAsy𝒫MA×𝒫MAsy|sx
22 elin y𝒫MA×𝒫MAsy𝒫MA×𝒫MAys
23 22 anbi1i y𝒫MA×𝒫MAsy|sxy𝒫MA×𝒫MAysy|sx
24 anass y𝒫MA×𝒫MAysy|sxy𝒫MA×𝒫MAysy|sx
25 23 24 bitri y𝒫MA×𝒫MAsy|sxy𝒫MA×𝒫MAysy|sx
26 25 rexbii2 y𝒫MA×𝒫MAsy|sxy𝒫MA×𝒫MAysy|sx
27 19 21 26 3bitri x|s𝒫MA×𝒫MAy𝒫MA×𝒫MAysy|sx
28 df-br asbabs
29 28 anbi1i asba|sb=xabsa|sb=x
30 df-ov a|sb=|sab
31 30 eqeq1i a|sb=x|sab=x
32 scutf |s:sNo
33 ffn |s:sNo|sFns
34 32 33 ax-mp |sFns
35 fnbrfvb |sFnsabs|sab=xab|sx
36 34 35 mpan abs|sab=xab|sx
37 31 36 syl5bb absa|sb=xab|sx
38 37 pm5.32i absa|sb=xabsab|sx
39 29 38 bitri asba|sb=xabsab|sx
40 39 2rexbii a𝒫MAb𝒫MAasba|sb=xa𝒫MAb𝒫MAabsab|sx
41 13 27 40 3bitr4i x|s𝒫MA×𝒫MAa𝒫MAb𝒫MAasba|sb=x
42 41 abbi2i |s𝒫MA×𝒫MA=x|a𝒫MAb𝒫MAasba|sb=x
43 df-rab xNo|a𝒫MAb𝒫MAasba|sb=x=x|xNoa𝒫MAb𝒫MAasba|sb=x
44 9 42 43 3eqtr4i |s𝒫MA×𝒫MA=xNo|a𝒫MAb𝒫MAasba|sb=x
45 1 44 eqtrdi AOnMA=xNo|a𝒫MAb𝒫MAasba|sb=x