Metamath Proof Explorer

Theorem oeoelem

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

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

Proof

Step Hyp Ref Expression
1 oeoelem.1 
 |-  A e. On
2 oeoelem.2 
 |-  (/) e. A
3 oveq2 
 |-  ( x = (/) -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o (/) ) )
4 oveq2 
 |-  ( x = (/) -> ( B .o x ) = ( B .o (/) ) )
5 4 oveq2d 
 |-  ( x = (/) -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o (/) ) ) )
6 3 5 eqeq12d 
 |-  ( x = (/) -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> ( ( A ^o B ) ^o (/) ) = ( A ^o ( B .o (/) ) ) ) )
7 oveq2 
 |-  ( x = y -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o y ) )
8 oveq2 
 |-  ( x = y -> ( B .o x ) = ( B .o y ) )
9 8 oveq2d 
 |-  ( x = y -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o y ) ) )
10 7 9 eqeq12d 
 |-  ( x = y -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> ( ( A ^o B ) ^o y ) = ( A ^o ( B .o y ) ) ) )
11 oveq2 
 |-  ( x = suc y -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o suc y ) )
12 oveq2 
 |-  ( x = suc y -> ( B .o x ) = ( B .o suc y ) )
13 12 oveq2d 
 |-  ( x = suc y -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o suc y ) ) )
14 11 13 eqeq12d 
 |-  ( 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 ) ) ) )
15 oveq2 
 |-  ( x = C -> ( ( A ^o B ) ^o x ) = ( ( A ^o B ) ^o C ) )
16 oveq2 
 |-  ( x = C -> ( B .o x ) = ( B .o C ) )
17 16 oveq2d 
 |-  ( x = C -> ( A ^o ( B .o x ) ) = ( A ^o ( B .o C ) ) )
18 15 17 eqeq12d 
 |-  ( x = C -> ( ( ( A ^o B ) ^o x ) = ( A ^o ( B .o x ) ) <-> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) ) )
19 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
20 1 19 mpan 
 |-  ( B e. On -> ( A ^o B ) e. On )
21 oe0 
 |-  ( ( A ^o B ) e. On -> ( ( A ^o B ) ^o (/) ) = 1o )
22 20 21 syl 
 |-  ( B e. On -> ( ( A ^o B ) ^o (/) ) = 1o )
23 om0 
 |-  ( B e. On -> ( B .o (/) ) = (/) )
24 23 oveq2d 
 |-  ( B e. On -> ( A ^o ( B .o (/) ) ) = ( A ^o (/) ) )
25 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
26 1 25 ax-mp 
 |-  ( A ^o (/) ) = 1o
27 24 26 eqtrdi 
 |-  ( B e. On -> ( A ^o ( B .o (/) ) ) = 1o )
28 22 27 eqtr4d 
 |-  ( B e. On -> ( ( A ^o B ) ^o (/) ) = ( A ^o ( B .o (/) ) ) )
29 oveq1 
 |-  ( ( ( 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 ) ) )
30 oesuc 
 |-  ( ( ( A ^o B ) e. On /\ y e. On ) -> ( ( A ^o B ) ^o suc y ) = ( ( ( A ^o B ) ^o y ) .o ( A ^o B ) ) )
31 20 30 sylan 
 |-  ( ( B e. On /\ y e. On ) -> ( ( A ^o B ) ^o suc y ) = ( ( ( A ^o B ) ^o y ) .o ( A ^o B ) ) )
32 omsuc 
 |-  ( ( B e. On /\ y e. On ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
33 32 oveq2d 
 |-  ( ( B e. On /\ y e. On ) -> ( A ^o ( B .o suc y ) ) = ( A ^o ( ( B .o y ) +o B ) ) )
34 omcl 
 |-  ( ( B e. On /\ y e. On ) -> ( B .o y ) e. On )
35 oeoa 
 |-  ( ( 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 ) ) )
36 1 35 mp3an1 
 |-  ( ( ( B .o y ) e. On /\ B e. On ) -> ( A ^o ( ( B .o y ) +o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
37 34 36 sylan 
 |-  ( ( ( 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 ) ) )
38 37 anabss1 
 |-  ( ( B e. On /\ y e. On ) -> ( A ^o ( ( B .o y ) +o B ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
39 33 38 eqtrd 
 |-  ( ( B e. On /\ y e. On ) -> ( A ^o ( B .o suc y ) ) = ( ( A ^o ( B .o y ) ) .o ( A ^o B ) ) )
40 31 39 eqeq12d 
 |-  ( ( 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 ) ) ) )
41 29 40 imbitrrid 
 |-  ( ( 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 ) ) ) )
42 41 expcom 
 |-  ( 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 ) ) ) ) )
43 iuneq2 
 |-  ( 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 ) ) )
44 vex 
 |-  x e. _V
45 oen0 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> (/) e. ( A ^o B ) )
46 2 45 mpan2 
 |-  ( ( A e. On /\ B e. On ) -> (/) e. ( A ^o B ) )
47 oelim 
 |-  ( ( ( ( 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 19 47 sylanl1 
 |-  ( ( ( ( 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 mpidan 
 |-  ( ( ( 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 ) )
50 1 49 mpanl1 
 |-  ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
51 44 50 mpanr1 
 |-  ( ( B e. On /\ Lim x ) -> ( ( A ^o B ) ^o x ) = U_ y e. x ( ( A ^o B ) ^o y ) )
52 omlim 
 |-  ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( B .o x ) = U_ y e. x ( B .o y ) )
53 44 52 mpanr1 
 |-  ( ( B e. On /\ Lim x ) -> ( B .o x ) = U_ y e. x ( B .o y ) )
54 53 oveq2d 
 |-  ( ( B e. On /\ Lim x ) -> ( A ^o ( B .o x ) ) = ( A ^o U_ y e. x ( B .o y ) ) )
55 limord 
 |-  ( Lim x -> Ord x )
56 ordelon 
 |-  ( ( Ord x /\ y e. x ) -> y e. On )
57 55 56 sylan 
 |-  ( ( Lim x /\ y e. x ) -> y e. On )
58 57 34 sylan2 
 |-  ( ( B e. On /\ ( Lim x /\ y e. x ) ) -> ( B .o y ) e. On )
59 58 anassrs 
 |-  ( ( ( B e. On /\ Lim x ) /\ y e. x ) -> ( B .o y ) e. On )
60 59 ralrimiva 
 |-  ( ( B e. On /\ Lim x ) -> A. y e. x ( B .o y ) e. On )
61 0ellim 
 |-  ( Lim x -> (/) e. x )
62 61 ne0d 
 |-  ( Lim x -> x =/= (/) )
63 62 adantl 
 |-  ( ( B e. On /\ Lim x ) -> x =/= (/) )
64 vex 
 |-  w e. _V
65 oelim 
 |-  ( ( ( A e. On /\ ( w e. _V /\ Lim w ) ) /\ (/) e. A ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
66 2 65 mpan2 
 |-  ( ( A e. On /\ ( w e. _V /\ Lim w ) ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
67 1 66 mpan 
 |-  ( ( w e. _V /\ Lim w ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
68 64 67 mpan 
 |-  ( Lim w -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
69 oewordi 
 |-  ( ( ( z e. On /\ w e. On /\ A e. On ) /\ (/) e. A ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
70 2 69 mpan2 
 |-  ( ( z e. On /\ w e. On /\ A e. On ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
71 1 70 mp3an3 
 |-  ( ( z e. On /\ w e. On ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
72 71 3impia 
 |-  ( ( z e. On /\ w e. On /\ z C_ w ) -> ( A ^o z ) C_ ( A ^o w ) )
73 68 72 onoviun 
 |-  ( ( 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 ) ) )
74 44 60 63 73 mp3an2i 
 |-  ( ( B e. On /\ Lim x ) -> ( A ^o U_ y e. x ( B .o y ) ) = U_ y e. x ( A ^o ( B .o y ) ) )
75 54 74 eqtrd 
 |-  ( ( B e. On /\ Lim x ) -> ( A ^o ( B .o x ) ) = U_ y e. x ( A ^o ( B .o y ) ) )
76 51 75 eqeq12d 
 |-  ( ( 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 ) ) ) )
77 43 76 imbitrrid 
 |-  ( ( 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 ) ) ) )
78 77 expcom 
 |-  ( 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 ) ) ) ) )
79 6 10 14 18 28 42 78 tfinds3 
 |-  ( C e. On -> ( B e. On -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) ) )
80 79 impcom 
 |-  ( ( B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )