Metamath Proof Explorer

Theorem genpass

Description: Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (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. )
genpass.4 
|- dom F = ( P. X. P. )
genpass.5 
|- ( ( f e. P. /\ g e. P. ) -> ( f F g ) e. P. )
genpass.6 
|- ( ( f G g ) G h ) = ( f G ( g G h ) )
Assertion genpass 
|- ( ( A F B ) F C ) = ( A F ( B F C ) )

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 genpass.4 
 |-  dom F = ( P. X. P. )
4 genpass.5 
 |-  ( ( f e. P. /\ g e. P. ) -> ( f F g ) e. P. )
5 genpass.6 
 |-  ( ( f G g ) G h ) = ( f G ( g G h ) )
6 1 2 genpelv 
 |-  ( ( B e. P. /\ C e. P. ) -> ( t e. ( B F C ) <-> E. g e. B E. h e. C t = ( g G h ) ) )
7 6 3adant1 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( t e. ( B F C ) <-> E. g e. B E. h e. C t = ( g G h ) ) )
8 7 anbi1d 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( t e. ( B F C ) /\ x = ( f G t ) ) <-> ( E. g e. B E. h e. C t = ( g G h ) /\ x = ( f G t ) ) ) )
9 8 exbidv 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( E. t ( t e. ( B F C ) /\ x = ( f G t ) ) <-> E. t ( E. g e. B E. h e. C t = ( g G h ) /\ x = ( f G t ) ) ) )
10 df-rex 
 |-  ( E. t e. ( B F C ) x = ( f G t ) <-> E. t ( t e. ( B F C ) /\ x = ( f G t ) ) )
11 ovex 
 |-  ( g G h ) e. _V
12 11 isseti 
 |-  E. t t = ( g G h )
13 12 biantrur 
 |-  ( x = ( ( f G g ) G h ) <-> ( E. t t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
14 19.41v 
 |-  ( E. t ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> ( E. t t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
15 13 14 bitr4i 
 |-  ( x = ( ( f G g ) G h ) <-> E. t ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
16 15 rexbii 
 |-  ( E. h e. C x = ( ( f G g ) G h ) <-> E. h e. C E. t ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
17 rexcom4 
 |-  ( E. h e. C E. t ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> E. t E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
18 16 17 bitri 
 |-  ( E. h e. C x = ( ( f G g ) G h ) <-> E. t E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
19 18 rexbii 
 |-  ( E. g e. B E. h e. C x = ( ( f G g ) G h ) <-> E. g e. B E. t E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
20 rexcom4 
 |-  ( E. g e. B E. t E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> E. t E. g e. B E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
21 oveq2 
 |-  ( t = ( g G h ) -> ( f G t ) = ( f G ( g G h ) ) )
22 21 5 eqtr4di 
 |-  ( t = ( g G h ) -> ( f G t ) = ( ( f G g ) G h ) )
23 22 eqeq2d 
 |-  ( t = ( g G h ) -> ( x = ( f G t ) <-> x = ( ( f G g ) G h ) ) )
24 23 pm5.32i 
 |-  ( ( t = ( g G h ) /\ x = ( f G t ) ) <-> ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
25 24 rexbii 
 |-  ( E. h e. C ( t = ( g G h ) /\ x = ( f G t ) ) <-> E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
26 r19.41v 
 |-  ( E. h e. C ( t = ( g G h ) /\ x = ( f G t ) ) <-> ( E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
27 25 26 bitr3i 
 |-  ( E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> ( E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
28 27 rexbii 
 |-  ( E. g e. B E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> E. g e. B ( E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
29 r19.41v 
 |-  ( E. g e. B ( E. h e. C t = ( g G h ) /\ x = ( f G t ) ) <-> ( E. g e. B E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
30 28 29 bitri 
 |-  ( E. g e. B E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> ( E. g e. B E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
31 30 exbii 
 |-  ( E. t E. g e. B E. h e. C ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> E. t ( E. g e. B E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
32 19 20 31 3bitri 
 |-  ( E. g e. B E. h e. C x = ( ( f G g ) G h ) <-> E. t ( E. g e. B E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
33 9 10 32 3bitr4g 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( E. t e. ( B F C ) x = ( f G t ) <-> E. g e. B E. h e. C x = ( ( f G g ) G h ) ) )
34 33 rexbidv 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( E. f e. A E. t e. ( B F C ) x = ( f G t ) <-> E. f e. A E. g e. B E. h e. C x = ( ( f G g ) G h ) ) )
35 4 caovcl 
 |-  ( ( B e. P. /\ C e. P. ) -> ( B F C ) e. P. )
36 1 2 genpelv 
 |-  ( ( A e. P. /\ ( B F C ) e. P. ) -> ( x e. ( A F ( B F C ) ) <-> E. f e. A E. t e. ( B F C ) x = ( f G t ) ) )
37 35 36 sylan2 
 |-  ( ( A e. P. /\ ( B e. P. /\ C e. P. ) ) -> ( x e. ( A F ( B F C ) ) <-> E. f e. A E. t e. ( B F C ) x = ( f G t ) ) )
38 37 3impb 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( x e. ( A F ( B F C ) ) <-> E. f e. A E. t e. ( B F C ) x = ( f G t ) ) )
39 4 caovcl 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) e. P. )
40 1 2 genpelv 
 |-  ( ( ( A F B ) e. P. /\ C e. P. ) -> ( x e. ( ( A F B ) F C ) <-> E. t e. ( A F B ) E. h e. C x = ( t G h ) ) )
41 39 40 stoic3 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( x e. ( ( A F B ) F C ) <-> E. t e. ( A F B ) E. h e. C x = ( t G h ) ) )
42 1 2 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( t e. ( A F B ) <-> E. f e. A E. g e. B t = ( f G g ) ) )
43 42 3adant3 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( t e. ( A F B ) <-> E. f e. A E. g e. B t = ( f G g ) ) )
44 43 anbi1d 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( t e. ( A F B ) /\ E. h e. C x = ( t G h ) ) <-> ( E. f e. A E. g e. B t = ( f G g ) /\ E. h e. C x = ( t G h ) ) ) )
45 44 exbidv 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( E. t ( t e. ( A F B ) /\ E. h e. C x = ( t G h ) ) <-> E. t ( E. f e. A E. g e. B t = ( f G g ) /\ E. h e. C x = ( t G h ) ) ) )
46 df-rex 
 |-  ( E. t e. ( A F B ) E. h e. C x = ( t G h ) <-> E. t ( t e. ( A F B ) /\ E. h e. C x = ( t G h ) ) )
47 19.41v 
 |-  ( E. t ( t = ( f G g ) /\ E. h e. C x = ( ( f G g ) G h ) ) <-> ( E. t t = ( f G g ) /\ E. h e. C x = ( ( f G g ) G h ) ) )
48 oveq1 
 |-  ( t = ( f G g ) -> ( t G h ) = ( ( f G g ) G h ) )
49 48 eqeq2d 
 |-  ( t = ( f G g ) -> ( x = ( t G h ) <-> x = ( ( f G g ) G h ) ) )
50 49 rexbidv 
 |-  ( t = ( f G g ) -> ( E. h e. C x = ( t G h ) <-> E. h e. C x = ( ( f G g ) G h ) ) )
51 50 pm5.32i 
 |-  ( ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) <-> ( t = ( f G g ) /\ E. h e. C x = ( ( f G g ) G h ) ) )
52 51 exbii 
 |-  ( E. t ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) <-> E. t ( t = ( f G g ) /\ E. h e. C x = ( ( f G g ) G h ) ) )
53 ovex 
 |-  ( f G g ) e. _V
54 53 isseti 
 |-  E. t t = ( f G g )
55 54 biantrur 
 |-  ( E. h e. C x = ( ( f G g ) G h ) <-> ( E. t t = ( f G g ) /\ E. h e. C x = ( ( f G g ) G h ) ) )
56 47 52 55 3bitr4ri 
 |-  ( E. h e. C x = ( ( f G g ) G h ) <-> E. t ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
57 56 rexbii 
 |-  ( E. g e. B E. h e. C x = ( ( f G g ) G h ) <-> E. g e. B E. t ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
58 rexcom4 
 |-  ( E. g e. B E. t ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) <-> E. t E. g e. B ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
59 57 58 bitri 
 |-  ( E. g e. B E. h e. C x = ( ( f G g ) G h ) <-> E. t E. g e. B ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
60 59 rexbii 
 |-  ( E. f e. A E. g e. B E. h e. C x = ( ( f G g ) G h ) <-> E. f e. A E. t E. g e. B ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
61 rexcom4 
 |-  ( E. f e. A E. t E. g e. B ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) <-> E. t E. f e. A E. g e. B ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
62 r19.41vv 
 |-  ( E. f e. A E. g e. B ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) <-> ( E. f e. A E. g e. B t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
63 62 exbii 
 |-  ( E. t E. f e. A E. g e. B ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) <-> E. t ( E. f e. A E. g e. B t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
64 60 61 63 3bitri 
 |-  ( E. f e. A E. g e. B E. h e. C x = ( ( f G g ) G h ) <-> E. t ( E. f e. A E. g e. B t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
65 45 46 64 3bitr4g 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( E. t e. ( A F B ) E. h e. C x = ( t G h ) <-> E. f e. A E. g e. B E. h e. C x = ( ( f G g ) G h ) ) )
66 41 65 bitrd 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( x e. ( ( A F B ) F C ) <-> E. f e. A E. g e. B E. h e. C x = ( ( f G g ) G h ) ) )
67 34 38 66 3bitr4rd 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( x e. ( ( A F B ) F C ) <-> x e. ( A F ( B F C ) ) ) )
68 67 eqrdv 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
69 0npr 
 |-  -. (/) e. P.
70 3 69 ndmovass 
 |-  ( -. ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
71 68 70 pm2.61i 
 |-  ( ( A F B ) F C ) = ( A F ( B F C ) )