Theorem oeoelem 7150

Description: Lemma for oeoe 7151. (Contributed by Eric Schmidt, 26-May-2009.)

Hypotheses

Ref	Expression
oeoelem.1	|- A e. On
oeoelem.2	|- (/) e. A

Assertion

Ref	Expression
oeoelem	|- ( ( B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )

Proof of Theorem oeoelem

Dummy variables x y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6211	. . . 4 |- ( x = (/) -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o (/) ) )
2		oveq2 6211	. . . . 5 |- ( x = (/) -> ( B .o x ) = ( B .o (/) ) )
3	2	oveq2d 6219	. . . 4 |- ( x = (/) -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o (/) ) ) )
4	1, 3	eqeq12d 2476	. . 3 |- ( x = (/) -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> ( ( A ^o B ) ^o (/) ) = ( A ^o ( B .o (/) ) ) ) )
5		oveq2 6211	. . . 4 |- ( x = y -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o y ) )
6		oveq2 6211	. . . . 5 |- ( x = y -> ( B .o x ) = ( B .o y ) )
7	6	oveq2d 6219	. . . 4 |- ( x = y -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o y ) ) )
8	5, 7	eqeq12d 2476	. . 3 |- ( x = y -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) ) )
9		oveq2 6211	. . . 4 |- ( x = suc y -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o suc y ) )
10		oveq2 6211	. . . . 5 |- ( x = suc y -> ( B .o x ) = ( B .o suc y ) )
11	10	oveq2d 6219	. . . 4 |- ( x = suc y -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o suc y ) ) )
12	9, 11	eqeq12d 2476	. . 3 |- ( x = suc y -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> ( ( A ^o B ) ^o suc y ) = ( A ^o ( B .o suc y ) ) ) )
13		oveq2 6211	. . . 4 |- ( x = C -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o C ) )
14		oveq2 6211	. . . . 5 |- ( x = C -> ( B .o x ) = ( B .o C ) )
15	14	oveq2d 6219	. . . 4 |- ( x = C -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o C ) ) )
16	13, 15	eqeq12d 2476	. . 3 |- ( x = C -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) ) )
17		oeoelem.1	. . . . . 6 |- A e. On
18		oecl 7090	. . . . . 6 |- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
19	17, 18	mpan 670	. . . . 5 |- ( B e. On -> ( A ^o B ) e. On )
20		oe0 7075	. . . . 5 |- ( ( A ^o B ) e. On -> ( ( A ^o B ) ^o (/) ) = 1o )
21	19, 20	syl 16	. . . 4 |- ( B e. On -> ( ( A ^o B ) ^o (/) ) = 1o )
22		om0 7070	. . . . . 6 |- ( B e. On -> ( B .o (/) ) = (/) )
23	22	oveq2d 6219	. . . . 5 |- ( B e. On -> ( A ^o ( B .o (/) ) ) = ( A ^o (/) ) )
24		oe0 7075	. . . . . 6 |- ( A e. On -> ( A ^o (/) ) = 1o )
25	17, 24	ax-mp 5	. . . . 5 |- ( A ^o (/) ) = 1o
26	23, 25	syl6eq 2511	. . . 4 |- ( B e. On -> ( A ^o ( B .o (/) ) ) = 1o )
27	21, 26	eqtr4d 2498	. . 3 |- ( B e. On -> ( ( A ^o B ) ^o (/) ) = ( A ^o ( B .o (/) ) ) )
28		oveq1 6210	. . . . 5 |- ( ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) -> ( ( ( A ^o B ) ^o y ) .o ( A ^o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
29		oesuc 7080	. . . . . . 7 |- ( ( ( A ^o B ) e. On /\ y e. On ) -> ( ( A ^o B ) ^o suc y ) = ( ( ( A ^o B ) ^o y ) .o ( A ^o B ) ) )
30	19, 29	sylan 471	. . . . . 6 |- ( ( B e. On /\ y e. On ) -> ( ( A ^o B ) ^o suc y ) = ( ( ( A ^o B ) ^o y ) .o ( A ^o B ) ) )
31		omsuc 7079	. . . . . . . 8 |- ( ( B e. On /\ y e. On ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
32	31	oveq2d 6219	. . . . . . 7 |- ( ( B e. On /\ y e. On ) -> ( A ^o ( B .o suc y ) ) = ( A ^o ( ( B .o y ) +o B ) ) )
33		omcl 7089	. . . . . . . . 9 |- ( ( B e. On /\ y e. On ) -> ( B .o y ) e. On )
34		oeoa 7149	. . . . . . . . . 10 |- ( ( A e. On /\ ( B .o y ) e. On /\ B e. On ) -> ( A ^o ( ( B .o y ) +o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
35	17, 34	mp3an1 1302	. . . . . . . . 9 |- ( ( ( B .o y ) e. On /\ B e. On ) -> ( A ^o ( ( B .o y ) +o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
36	33, 35	sylan 471	. . . . . . . 8 |- ( ( ( B e. On /\ y e. On ) /\ B e. On ) -> ( A ^o ( ( B .o y ) +o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
37	36	anabss1 810	. . . . . . 7 |- ( ( B e. On /\ y e. On ) -> ( A ^o ( ( B .o y ) +o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
38	32, 37	eqtrd 2495	. . . . . 6 |- ( ( B e. On /\ y e. On ) -> ( A ^o ( B .o suc y ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
39	30, 38	eqeq12d 2476	. . . . 5 |- ( ( B e. On /\ y e. On ) -> ( ( ( A ^o B ) ^o suc y ) = ( A ^o ( B .o suc y ) ) <-> ( ( ( A ^o B ) ^o y ) .o ( A ^o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) ) )
40	28, 39	syl5ibr 221	. . . 4 |- ( ( B e. On /\ y e. On ) -> ( ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) -> ( ( A ^o B ) ^o suc y ) = ( A ^o ( B .o suc y ) ) ) )
41	40	expcom 435	. . 3 |- ( y e. On -> ( B e. On -> ( ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) -> ( ( A ^o B ) ^o suc y ) = ( A ^o ( B .o suc y ) ) ) ) )
42		iuneq2 4298	. . . . 5 |- ( A. y e. x ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) -> U_ y e. x ( ( A ^o B ) ^o y ) = U_ y e. x ( A ^o ( B .o y ) ) )
43		vex 3081	. . . . . . 7 |- x e. _V
44		oeoelem.2	. . . . . . . . . . 11 |- (/) e. A
45		oen0 7138	. . . . . . . . . . 11 |- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> (/) e. ( A ^o B ) )
46	44, 45	mpan2 671	. . . . . . . . . 10 |- ( ( A e. On /\ B e. On ) -> (/) e. ( A ^o B ) )
47		oelim 7087	. . . . . . . . . . 11 |- ( ( ( ( A ^o B ) e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. ( A ^o B ) ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
48	18, 47	sylanl1 650	. . . . . . . . . 10 |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. _V /\ Lim x ) ) /\ (/) e. ( A ^o B ) ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
49	46, 48	sylan2 474	. . . . . . . . 9 |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. _V /\ Lim x ) ) /\ ( A e. On /\ B e. On ) ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
50	49	anabss1 810	. . . . . . . 8 |- ( ( ( A e. On /\ B e. On ) /\ ( x e. _V /\ Lim x ) ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
51	17, 50	mpanl1 680	. . . . . . 7 |- ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
52	43, 51	mpanr1 683	. . . . . 6 |- ( ( B e. On /\ Lim x ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
53		omlim 7086	. . . . . . . . 9 |- ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( B .o x ) = U_ y e. x ( B .o y ) )
54	43, 53	mpanr1 683	. . . . . . . 8 |- ( ( B e. On /\ Lim x ) -> ( B .o x ) = U_ y e. x ( B .o y ) )
55	54	oveq2d 6219	. . . . . . 7 |- ( ( B e. On /\ Lim x ) -> ( A ^o ( B .o x ) ) = ( A ^o U_ y e. x ( B .o y ) ) )
56	43	a1i 11	. . . . . . . 8 |- ( ( B e. On /\ Lim x ) -> x e. _V )
57		limord 4889	. . . . . . . . . . . 12 |- ( Lim x -> Ord x )
58		ordelon 4854	. . . . . . . . . . . 12 |- ( ( Ord x /\ y e. x ) -> y e. On )
59	57, 58	sylan 471	. . . . . . . . . . 11 |- ( ( Lim x /\ y e. x ) -> y e. On )
60	59, 33	sylan2 474	. . . . . . . . . 10 |- ( ( B e. On /\ ( Lim x /\ y e. x ) ) -> ( B .o y ) e. On )
61	60	anassrs 648	. . . . . . . . 9 |- ( ( ( B e. On /\ Lim x ) /\ y e. x ) -> ( B .o y ) e. On )
62	61	ralrimiva 2830	. . . . . . . 8 |- ( ( B e. On /\ Lim x ) -> A. y e. x ( B .o y ) e. On )
63		0ellim 4892	. . . . . . . . . 10 |- ( Lim x -> (/) e. x )
64		ne0i 3754	. . . . . . . . . 10 |- ( (/) e. x -> x =/= (/) )
65	63, 64	syl 16	. . . . . . . . 9 |- ( Lim x -> x =/= (/) )
66	65	adantl 466	. . . . . . . 8 |- ( ( B e. On /\ Lim x ) -> x =/= (/) )
67		vex 3081	. . . . . . . . . 10 |- w e. _V
68		oelim 7087	. . . . . . . . . . . 12 |- ( ( ( A e. On /\ ( w e. _V /\ Lim w ) ) /\ (/) e. A ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
69	44, 68	mpan2 671	. . . . . . . . . . 11 |- ( ( A e. On /\ ( w e. _V /\ Lim w ) ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
70	17, 69	mpan 670	. . . . . . . . . 10 |- ( ( w e. _V /\ Lim w ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
71	67, 70	mpan 670	. . . . . . . . 9 |- ( Lim w -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
72		oewordi 7143	. . . . . . . . . . . 12 |- ( ( ( z e. On /\ w e. On /\ A e. On ) /\ (/) e. A ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
73	44, 72	mpan2 671	. . . . . . . . . . 11 |- ( ( z e. On /\ w e. On /\ A e. On ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
74	17, 73	mp3an3 1304	. . . . . . . . . 10 |- ( ( z e. On /\ w e. On ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
75	74	3impia 1185	. . . . . . . . 9 |- ( ( z e. On /\ w e. On /\ z C_ w ) -> ( A ^o z ) C_ ( A ^o w ) )
76	71, 75	onoviun 6917	. . . . . . . 8 |- ( ( x e. _V /\ A. y e. x ( B .o y ) e. On /\ x =/= (/) ) -> ( A ^o U_ y e. x ( B .o y ) ) = U_ y e. x ( A ^o ( B .o y ) ) )
77	56, 62, 66, 76	syl3anc 1219	. . . . . . 7 |- ( ( B e. On /\ Lim x ) -> ( A ^o U_ y e. x ( B .o y ) ) = U_ y e. x ( A ^o ( B .o y ) ) )
78	55, 77	eqtrd 2495	. . . . . 6 |- ( ( B e. On /\ Lim x ) -> ( A ^o ( B .o x ) ) = U_ y e. x ( A ^o ( B .o y ) ) )
79	52, 78	eqeq12d 2476	. . . . 5 |- ( ( B e. On /\ Lim x ) -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> U_ y e. x ( ( A ^o B ) ^o y ) = U_ y e. x ( A ^o ( B .o y ) ) ) )
80	42, 79	syl5ibr 221	. . . 4 |- ( ( B e. On /\ Lim x ) -> ( A. y e. x ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) -> ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) ) )
81	80	expcom 435	. . 3 |- ( Lim x -> ( B e. On -> ( A. y e. x ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) -> ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) ) ) )
82	4, 8, 12, 16, 27, 41, 81	tfinds3 6588	. 2 |- ( C e. On -> ( B e. On -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) ) )
83	82	impcom 430	1 |- ( ( B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   =/= wne 2648   A.wral 2799   _Vcvv 3078   C_ wss 3439   (/)c0 3748   U_ciun 4282   Ord word 4829   Oncon0 4830   Lim wlim 4831   suc csuc 4832  (class class class)co 6203   1oc1o 7026   +o coa 7030   .o comu 7031   ^o coe 7032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-om 6590  df-1st 6690  df-2nd 6691  df-recs 6945  df-rdg 6979  df-1o 7033  df-2o 7034  df-oadd 7037  df-omul 7038  df-oexp 7039

This theorem is referenced by:  oeoe  7151