Metamath Proof Explorer

Theorem madeval2

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

Ref Expression
Assertion madeval2 
|- ( A e. On -> ( _M ` A ) = { x e. No | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <

Proof

Step Hyp Ref Expression
1 madeval 
 |-  ( A e. On -> ( _M ` A ) = ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) )
2 scutcl 
 |-  ( a < ( a |s b ) e. No )
3 eleq1 
 |-  ( ( a |s b ) = x -> ( ( a |s b ) e. No <-> x e. No ) )
4 3 biimpd 
 |-  ( ( a |s b ) = x -> ( ( a |s b ) e. No -> x e. No ) )
5 2 4 mpan9 
 |-  ( ( a < x e. No )
6 5 rexlimivw 
 |-  ( E. b e. ~P U. ( _M " A ) ( a < x e. No )
7 6 rexlimivw 
 |-  ( E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a < x e. No )
8 7 pm4.71ri 
 |-  ( E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a < ( x e. No /\ E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
9 8 abbii 
 |-  { x | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
10 eleq1 
 |-  ( y = <. a , b >. -> ( y e. < <. a , b >. e. <
11 breq1 
 |-  ( y = <. a , b >. -> ( y |s x <-> <. a , b >. |s x ) )
12 10 11 anbi12d 
 |-  ( y = <. a , b >. -> ( ( y e. < ( <. a , b >. e. <. |s x ) ) )
13 12 rexxp 
 |-  ( E. y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ( y e. < E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( <. a , b >. e. <. |s x ) )
14 imaindm 
 |-  ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) = ( |s " ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i dom |s ) )
15 dmscut 
 |-  dom |s = <
16 15 ineq2i 
 |-  ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i dom |s ) = ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i <
17 16 imaeq2i 
 |-  ( |s " ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i dom |s ) ) = ( |s " ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i <
18 14 17 eqtri 
 |-  ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) = ( |s " ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i <
19 18 eleq2i 
 |-  ( x e. ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) <-> x e. ( |s " ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i <
20 vex 
 |-  x e. _V
21 20 elima 
 |-  ( x e. ( |s " ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i < E. y e. ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i <
22 elin 
 |-  ( y e. ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i < ( y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) /\ y e. <
23 22 anbi1i 
 |-  ( ( y e. ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i < ( ( y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) /\ y e. <
24 anass 
 |-  ( ( ( y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) /\ y e. < ( y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) /\ ( y e. <
25 23 24 bitri 
 |-  ( ( y e. ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i < ( y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) /\ ( y e. <
26 25 rexbii2 
 |-  ( E. y e. ( ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) i^i < E. y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ( y e. <
27 19 21 26 3bitri 
 |-  ( x e. ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) <-> E. y e. ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ( y e. <
28 df-br 
 |-  ( a < <. a , b >. e. <
29 28 anbi1i 
 |-  ( ( a < ( <. a , b >. e. <
30 df-ov 
 |-  ( a |s b ) = ( |s ` <. a , b >. )
31 30 eqeq1i 
 |-  ( ( a |s b ) = x <-> ( |s ` <. a , b >. ) = x )
32 scutf 
 |-  |s : < No
33 ffn 
 |-  ( |s : < No -> |s Fn <
34 32 33 ax-mp 
 |-  |s Fn <
35 fnbrfvb 
 |-  ( ( |s Fn <. e. < ( ( |s ` <. a , b >. ) = x <-> <. a , b >. |s x ) )
36 34 35 mpan 
 |-  ( <. a , b >. e. < ( ( |s ` <. a , b >. ) = x <-> <. a , b >. |s x ) )
37 31 36 syl5bb 
 |-  ( <. a , b >. e. < ( ( a |s b ) = x <-> <. a , b >. |s x ) )
38 37 pm5.32i 
 |-  ( ( <. a , b >. e. < ( <. a , b >. e. <. |s x ) )
39 29 38 bitri 
 |-  ( ( a < ( <. a , b >. e. <. |s x ) )
40 39 2rexbii 
 |-  ( E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a < E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( <. a , b >. e. <. |s x ) )
41 13 27 40 3bitr4i 
 |-  ( x e. ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) <-> E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
42 41 abbi2i 
 |-  ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) = { x | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
43 df-rab 
 |-  { x e. No | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
44 9 42 43 3eqtr4i 
 |-  ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) = { x e. No | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <
45 1 44 eqtrdi 
 |-  ( A e. On -> ( _M ` A ) = { x e. No | E. a e. ~P U. ( _M " A ) E. b e. ~P U. ( _M " A ) ( a <