Theorem genpass 9831

Description: Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)

Hypotheses

Ref	Expression
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

Ref	Expression
genpass	|- ( ( A F B ) F C ) = ( A F ( B F C ) )

Distinct variable groups:   x, y, z, f, g, h, A   x, B, y, z, f, g, h   x, w, v, G, y, z, f, g, h   f, F, g   C, f, g, h, x, y, z   x, F, y, z, h

Allowed substitution hints:   A( w, v)   B( w, v)   C( w, v)   F( w, v)

Proof of Theorem genpass

Dummy variable t is distinct from all other variables.

Step	Hyp	Ref	Expression
1		genp.1	. . . . . . . . . 10 |- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
2		genp.2	. . . . . . . . . 10 |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
3	1, 2	genpelv 9822	. . . . . . . . 9 |- ( ( B e. P. /\ C e. P. ) -> ( t e. ( B F C ) <-> E. g e. B E. h e. C t = ( g G h ) ) )
4	3	3adant1 1079	. . . . . . . 8 |- ( ( 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 ) ) )
5	4	anbi1d 741	. . . . . . 7 |- ( ( 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 ) ) ) )
6	5	exbidv 1850	. . . . . 6 |- ( ( 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 ) ) ) )
7		df-rex 2918	. . . . . 6 |- ( E. t e. ( B F C ) x = ( f G t ) <-> E. t ( t e. ( B F C ) /\ x = ( f G t ) ) )
8		ovex 6678	. . . . . . . . . . . . 13 |- ( g G h ) e. _V
9	8	isseti 3209	. . . . . . . . . . . 12 |- E. t t = ( g G h )
10	9	biantrur 527	. . . . . . . . . . 11 |- ( x = ( ( f G g ) G h ) <-> ( E. t t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
11		19.41v 1914	. . . . . . . . . . 11 |- ( E. t ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) <-> ( E. t t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
12	10, 11	bitr4i 267	. . . . . . . . . 10 |- ( x = ( ( f G g ) G h ) <-> E. t ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
13	12	rexbii 3041	. . . . . . . . 9 |- ( 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 ) ) )
14		rexcom4 3225	. . . . . . . . 9 |- ( 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 ) ) )
15	13, 14	bitri 264	. . . . . . . 8 |- ( 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 ) ) )
16	15	rexbii 3041	. . . . . . 7 |- ( 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 ) ) )
17		rexcom4 3225	. . . . . . 7 |- ( 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 ) ) )
18		oveq2 6658	. . . . . . . . . . . . . . 15 |- ( t = ( g G h ) -> ( f G t ) = ( f G ( g G h ) ) )
19		genpass.6	. . . . . . . . . . . . . . 15 |- ( ( f G g ) G h ) = ( f G ( g G h ) )
20	18, 19	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( t = ( g G h ) -> ( f G t ) = ( ( f G g ) G h ) )
21	20	eqeq2d 2632	. . . . . . . . . . . . 13 |- ( t = ( g G h ) -> ( x = ( f G t ) <-> x = ( ( f G g ) G h ) ) )
22	21	pm5.32i 669	. . . . . . . . . . . 12 |- ( ( t = ( g G h ) /\ x = ( f G t ) ) <-> ( t = ( g G h ) /\ x = ( ( f G g ) G h ) ) )
23	22	rexbii 3041	. . . . . . . . . . 11 |- ( 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 ) ) )
24		r19.41v 3089	. . . . . . . . . . 11 |- ( E. h e. C ( t = ( g G h ) /\ x = ( f G t ) ) <-> ( E. h e. C t = ( g G h ) /\ x = ( f G t ) ) )
25	23, 24	bitr3i 266	. . . . . . . . . 10 |- ( 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 ) ) )
26	25	rexbii 3041	. . . . . . . . 9 |- ( 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 ) ) )
27		r19.41v 3089	. . . . . . . . 9 |- ( 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 ) ) )
28	26, 27	bitri 264	. . . . . . . 8 |- ( 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	28	exbii 1774	. . . . . . 7 |- ( 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 ) ) )
30	16, 17, 29	3bitri 286	. . . . . 6 |- ( 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 ) ) )
31	6, 7, 30	3bitr4g 303	. . . . 5 |- ( ( 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 ) ) )
32	31	rexbidv 3052	. . . 4 |- ( ( 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 ) ) )
33		genpass.5	. . . . . . 7 |- ( ( f e. P. /\ g e. P. ) -> ( f F g ) e. P. )
34	33	caovcl 6828	. . . . . 6 |- ( ( B e. P. /\ C e. P. ) -> ( B F C ) e. P. )
35	1, 2	genpelv 9822	. . . . . 6 |- ( ( 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 ) ) )
36	34, 35	sylan2 491	. . . . 5 |- ( ( 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 ) ) )
37	36	3impb 1260	. . . 4 |- ( ( 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	33	caovcl 6828	. . . . . 6 |- ( ( A e. P. /\ B e. P. ) -> ( A F B ) e. P. )
39	1, 2	genpelv 9822	. . . . . 6 |- ( ( ( 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 ) ) )
40	38, 39	stoic3 1701	. . . . 5 |- ( ( 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 ) ) )
41	1, 2	genpelv 9822	. . . . . . . . 9 |- ( ( A e. P. /\ B e. P. ) -> ( t e. ( A F B ) <-> E. f e. A E. g e. B t = ( f G g ) ) )
42	41	3adant3 1081	. . . . . . . 8 |- ( ( 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 ) ) )
43	42	anbi1d 741	. . . . . . 7 |- ( ( 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 ) ) ) )
44	43	exbidv 1850	. . . . . 6 |- ( ( 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 ) ) ) )
45		df-rex 2918	. . . . . 6 |- ( 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 ) ) )
46		19.41v 1914	. . . . . . . . . . 11 |- ( 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 ) ) )
47		oveq1 6657	. . . . . . . . . . . . . . 15 |- ( t = ( f G g ) -> ( t G h ) = ( ( f G g ) G h ) )
48	47	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( t = ( f G g ) -> ( x = ( t G h ) <-> x = ( ( f G g ) G h ) ) )
49	48	rexbidv 3052	. . . . . . . . . . . . 13 |- ( t = ( f G g ) -> ( E. h e. C x = ( t G h ) <-> E. h e. C x = ( ( f G g ) G h ) ) )
50	49	pm5.32i 669	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
51	50	exbii 1774	. . . . . . . . . . 11 |- ( 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 ) ) )
52		ovex 6678	. . . . . . . . . . . . 13 |- ( f G g ) e. _V
53	52	isseti 3209	. . . . . . . . . . . 12 |- E. t t = ( f G g )
54	53	biantrur 527	. . . . . . . . . . 11 |- ( 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 ) ) )
55	46, 51, 54	3bitr4ri 293	. . . . . . . . . 10 |- ( E. h e. C x = ( ( f G g ) G h ) <-> E. t ( t = ( f G g ) /\ E. h e. C x = ( t G h ) ) )
56	55	rexbii 3041	. . . . . . . . 9 |- ( 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 ) ) )
57		rexcom4 3225	. . . . . . . . 9 |- ( 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 ) ) )
58	56, 57	bitri 264	. . . . . . . 8 |- ( 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 ) ) )
59	58	rexbii 3041	. . . . . . 7 |- ( 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 ) ) )
60		rexcom4 3225	. . . . . . 7 |- ( 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 ) ) )
61		r19.41vv 3091	. . . . . . . 8 |- ( 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 ) ) )
62	61	exbii 1774	. . . . . . 7 |- ( 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 ) ) )
63	59, 60, 62	3bitri 286	. . . . . 6 |- ( 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 ) ) )
64	44, 45, 63	3bitr4g 303	. . . . 5 |- ( ( 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 ) ) )
65	40, 64	bitrd 268	. . . 4 |- ( ( 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 ) ) )
66	32, 37, 65	3bitr4rd 301	. . 3 |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( x e. ( ( A F B ) F C ) <-> x e. ( A F ( B F C ) ) ) )
67	66	eqrdv 2620	. 2 |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
68		genpass.4	. . 3 |- dom F = ( P. X. P. )
69		0npr 9814	. . 3 |- -. (/) e. P.
70	68, 69	ndmovass 6822	. 2 |- ( -. ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
71	67, 70	pm2.61i 176	1 |- ( ( A F B ) F C ) = ( A F ( B F C ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   E.wrex 2913   X. cxp 5112   dom cdm 5114  (class class class)co 6650   |-> cmpt2 6652   Q.cnq 9674   P.cnp 9681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-ni 9694  df-nq 9734  df-np 9803

This theorem is referenced by:  addasspr  9844  mulasspr  9846