Metamath Proof Explorer


Theorem oeoelem

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

Ref Expression
Hypotheses oeoelem.1 A On
oeoelem.2 A
Assertion oeoelem B On C On A 𝑜 B 𝑜 C = A 𝑜 B 𝑜 C

Proof

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