This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem genpcl

Description: Closure of an operation on reals. (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
genp.2 
|- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
genpcl.3 
|- ( h e. Q. -> ( f  ( h G f )
genpcl.4 
|- ( x G y ) = ( y G x )
genpcl.5 
|- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A F B ) ) )
Assertion genpcl 
|- ( ( A e. P. /\ B e. P. ) -> ( A F B ) e. P. )

Proof

Step Hyp Ref Expression
1 genp.1 
 |-  F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
2 genp.2 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
3 genpcl.3 
 |-  ( h e. Q. -> ( f  ( h G f )
4 genpcl.4 
 |-  ( x G y ) = ( y G x )
5 genpcl.5 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A F B ) ) )
6 1 2 genpn0 
 |-  ( ( A e. P. /\ B e. P. ) -> (/) C. ( A F B ) )
7 1 2 genpss 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) C_ Q. )
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 8 9 3 caovord 
 |-  ( z e. Q. -> ( x  ( z G x )
11 1 2 10 4 genpnnp 
 |-  ( ( A e. P. /\ B e. P. ) -> -. ( A F B ) = Q. )
12 dfpss2 
 |-  ( ( A F B ) C. Q. <-> ( ( A F B ) C_ Q. /\ -. ( A F B ) = Q. ) )
13 7 11 12 sylanbrc 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) C. Q. )
14 1 2 5 genpcd 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> ( x  x e. ( A F B ) ) ) )
15 14 alrimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> A. x ( x  x e. ( A F B ) ) ) )
16 vex 
 |-  z e. _V
17 vex 
 |-  w e. _V
18 16 17 3 caovord 
 |-  ( v e. Q. -> ( z  ( v G z )
19 16 17 4 caovcom 
 |-  ( z G w ) = ( w G z )
20 1 2 18 19 genpnmax 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> E. x e. ( A F B ) f
21 15 20 jcad 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> ( A. x ( x  x e. ( A F B ) ) /\ E. x e. ( A F B ) f
22 21 ralrimiv 
 |-  ( ( A e. P. /\ B e. P. ) -> A. f e. ( A F B ) ( A. x ( x  x e. ( A F B ) ) /\ E. x e. ( A F B ) f
23 elnp 
 |-  ( ( A F B ) e. P. <-> ( ( (/) C. ( A F B ) /\ ( A F B ) C. Q. ) /\ A. f e. ( A F B ) ( A. x ( x  x e. ( A F B ) ) /\ E. x e. ( A F B ) f
24 6 13 22 23 syl21anbrc 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) e. P. )