MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oeoa Structured version   Visualization version   GIF version

Theorem oeoa 8597
Description: Sum of exponents law for ordinal exponentiation. Theorem 8R of [Enderton] p. 238. Also Proposition 8.41 of [TakeutiZaring] p. 69. Theorem 4.7 of [Schloeder] p. 14. (Contributed by Eric Schmidt, 26-May-2009.)
Assertion
Ref Expression
oeoa ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)))

Proof of Theorem oeoa
StepHypRef Expression
1 oa00 8559 . . . . . . . . 9 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((๐ต +o ๐ถ) = โˆ… โ†” (๐ต = โˆ… โˆง ๐ถ = โˆ…)))
21biimpar 479 . . . . . . . 8 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง (๐ต = โˆ… โˆง ๐ถ = โˆ…)) โ†’ (๐ต +o ๐ถ) = โˆ…)
32oveq2d 7425 . . . . . . 7 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง (๐ต = โˆ… โˆง ๐ถ = โˆ…)) โ†’ (โˆ… โ†‘o (๐ต +o ๐ถ)) = (โˆ… โ†‘o โˆ…))
4 oveq2 7417 . . . . . . . . . 10 (๐ต = โˆ… โ†’ (โˆ… โ†‘o ๐ต) = (โˆ… โ†‘o โˆ…))
5 oveq2 7417 . . . . . . . . . . 11 (๐ถ = โˆ… โ†’ (โˆ… โ†‘o ๐ถ) = (โˆ… โ†‘o โˆ…))
6 oe0m0 8520 . . . . . . . . . . 11 (โˆ… โ†‘o โˆ…) = 1o
75, 6eqtrdi 2789 . . . . . . . . . 10 (๐ถ = โˆ… โ†’ (โˆ… โ†‘o ๐ถ) = 1o)
84, 7oveqan12d 7428 . . . . . . . . 9 ((๐ต = โˆ… โˆง ๐ถ = โˆ…) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = ((โˆ… โ†‘o โˆ…) ยทo 1o))
9 0elon 6419 . . . . . . . . . . 11 โˆ… โˆˆ On
10 oecl 8537 . . . . . . . . . . 11 ((โˆ… โˆˆ On โˆง โˆ… โˆˆ On) โ†’ (โˆ… โ†‘o โˆ…) โˆˆ On)
119, 9, 10mp2an 691 . . . . . . . . . 10 (โˆ… โ†‘o โˆ…) โˆˆ On
12 om1 8542 . . . . . . . . . 10 ((โˆ… โ†‘o โˆ…) โˆˆ On โ†’ ((โˆ… โ†‘o โˆ…) ยทo 1o) = (โˆ… โ†‘o โˆ…))
1311, 12ax-mp 5 . . . . . . . . 9 ((โˆ… โ†‘o โˆ…) ยทo 1o) = (โˆ… โ†‘o โˆ…)
148, 13eqtrdi 2789 . . . . . . . 8 ((๐ต = โˆ… โˆง ๐ถ = โˆ…) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = (โˆ… โ†‘o โˆ…))
1514adantl 483 . . . . . . 7 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง (๐ต = โˆ… โˆง ๐ถ = โˆ…)) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = (โˆ… โ†‘o โˆ…))
163, 15eqtr4d 2776 . . . . . 6 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง (๐ต = โˆ… โˆง ๐ถ = โˆ…)) โ†’ (โˆ… โ†‘o (๐ต +o ๐ถ)) = ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)))
17 oacl 8535 . . . . . . . . . 10 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (๐ต +o ๐ถ) โˆˆ On)
18 on0eln0 6421 . . . . . . . . . 10 ((๐ต +o ๐ถ) โˆˆ On โ†’ (โˆ… โˆˆ (๐ต +o ๐ถ) โ†” (๐ต +o ๐ถ) โ‰  โˆ…))
1917, 18syl 17 . . . . . . . . 9 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ต +o ๐ถ) โ†” (๐ต +o ๐ถ) โ‰  โˆ…))
20 oe0m1 8521 . . . . . . . . . 10 ((๐ต +o ๐ถ) โˆˆ On โ†’ (โˆ… โˆˆ (๐ต +o ๐ถ) โ†” (โˆ… โ†‘o (๐ต +o ๐ถ)) = โˆ…))
2117, 20syl 17 . . . . . . . . 9 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ต +o ๐ถ) โ†” (โˆ… โ†‘o (๐ต +o ๐ถ)) = โˆ…))
221necon3abid 2978 . . . . . . . . 9 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((๐ต +o ๐ถ) โ‰  โˆ… โ†” ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…)))
2319, 21, 223bitr3d 309 . . . . . . . 8 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((โˆ… โ†‘o (๐ต +o ๐ถ)) = โˆ… โ†” ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…)))
2423biimpar 479 . . . . . . 7 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…)) โ†’ (โˆ… โ†‘o (๐ต +o ๐ถ)) = โˆ…)
25 on0eln0 6421 . . . . . . . . . . . 12 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” ๐ต โ‰  โˆ…))
2625adantr 482 . . . . . . . . . . 11 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ต โ†” ๐ต โ‰  โˆ…))
27 on0eln0 6421 . . . . . . . . . . . 12 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†” ๐ถ โ‰  โˆ…))
2827adantl 483 . . . . . . . . . . 11 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ถ โ†” ๐ถ โ‰  โˆ…))
2926, 28orbi12d 918 . . . . . . . . . 10 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((โˆ… โˆˆ ๐ต โˆจ โˆ… โˆˆ ๐ถ) โ†” (๐ต โ‰  โˆ… โˆจ ๐ถ โ‰  โˆ…)))
30 neorian 3038 . . . . . . . . . 10 ((๐ต โ‰  โˆ… โˆจ ๐ถ โ‰  โˆ…) โ†” ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…))
3129, 30bitrdi 287 . . . . . . . . 9 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((โˆ… โˆˆ ๐ต โˆจ โˆ… โˆˆ ๐ถ) โ†” ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…)))
32 oe0m1 8521 . . . . . . . . . . . . . . 15 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
3332biimpa 478 . . . . . . . . . . . . . 14 ((๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต) โ†’ (โˆ… โ†‘o ๐ต) = โˆ…)
3433oveq1d 7424 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = (โˆ… ยทo (โˆ… โ†‘o ๐ถ)))
35 oecl 8537 . . . . . . . . . . . . . . 15 ((โˆ… โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (โˆ… โ†‘o ๐ถ) โˆˆ On)
369, 35mpan 689 . . . . . . . . . . . . . 14 (๐ถ โˆˆ On โ†’ (โˆ… โ†‘o ๐ถ) โˆˆ On)
37 om0r 8539 . . . . . . . . . . . . . 14 ((โˆ… โ†‘o ๐ถ) โˆˆ On โ†’ (โˆ… ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
3836, 37syl 17 . . . . . . . . . . . . 13 (๐ถ โˆˆ On โ†’ (โˆ… ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
3934, 38sylan9eq 2793 . . . . . . . . . . . 12 (((๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต) โˆง ๐ถ โˆˆ On) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
4039an32s 651 . . . . . . . . . . 11 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
41 oe0m1 8521 . . . . . . . . . . . . . . 15 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†” (โˆ… โ†‘o ๐ถ) = โˆ…))
4241biimpa 478 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ On โˆง โˆ… โˆˆ ๐ถ) โ†’ (โˆ… โ†‘o ๐ถ) = โˆ…)
4342oveq2d 7425 . . . . . . . . . . . . 13 ((๐ถ โˆˆ On โˆง โˆ… โˆˆ ๐ถ) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = ((โˆ… โ†‘o ๐ต) ยทo โˆ…))
44 oecl 8537 . . . . . . . . . . . . . . 15 ((โˆ… โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โˆ… โ†‘o ๐ต) โˆˆ On)
459, 44mpan 689 . . . . . . . . . . . . . 14 (๐ต โˆˆ On โ†’ (โˆ… โ†‘o ๐ต) โˆˆ On)
46 om0 8517 . . . . . . . . . . . . . 14 ((โˆ… โ†‘o ๐ต) โˆˆ On โ†’ ((โˆ… โ†‘o ๐ต) ยทo โˆ…) = โˆ…)
4745, 46syl 17 . . . . . . . . . . . . 13 (๐ต โˆˆ On โ†’ ((โˆ… โ†‘o ๐ต) ยทo โˆ…) = โˆ…)
4843, 47sylan9eqr 2795 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง (๐ถ โˆˆ On โˆง โˆ… โˆˆ ๐ถ)) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
4948anassrs 469 . . . . . . . . . . 11 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง โˆ… โˆˆ ๐ถ) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
5040, 49jaodan 957 . . . . . . . . . 10 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง (โˆ… โˆˆ ๐ต โˆจ โˆ… โˆˆ ๐ถ)) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
5150ex 414 . . . . . . . . 9 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((โˆ… โˆˆ ๐ต โˆจ โˆ… โˆˆ ๐ถ) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…))
5231, 51sylbird 260 . . . . . . . 8 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…))
5352imp 408 . . . . . . 7 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…)) โ†’ ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)) = โˆ…)
5424, 53eqtr4d 2776 . . . . . 6 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง ยฌ (๐ต = โˆ… โˆง ๐ถ = โˆ…)) โ†’ (โˆ… โ†‘o (๐ต +o ๐ถ)) = ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)))
5516, 54pm2.61dan 812 . . . . 5 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (โˆ… โ†‘o (๐ต +o ๐ถ)) = ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)))
56 oveq1 7416 . . . . . 6 (๐ด = โˆ… โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = (โˆ… โ†‘o (๐ต +o ๐ถ)))
57 oveq1 7416 . . . . . . 7 (๐ด = โˆ… โ†’ (๐ด โ†‘o ๐ต) = (โˆ… โ†‘o ๐ต))
58 oveq1 7416 . . . . . . 7 (๐ด = โˆ… โ†’ (๐ด โ†‘o ๐ถ) = (โˆ… โ†‘o ๐ถ))
5957, 58oveq12d 7427 . . . . . 6 (๐ด = โˆ… โ†’ ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)) = ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ)))
6056, 59eqeq12d 2749 . . . . 5 (๐ด = โˆ… โ†’ ((๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)) โ†” (โˆ… โ†‘o (๐ต +o ๐ถ)) = ((โˆ… โ†‘o ๐ต) ยทo (โˆ… โ†‘o ๐ถ))))
6155, 60imbitrrid 245 . . . 4 (๐ด = โˆ… โ†’ ((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ))))
6261impcom 409 . . 3 (((๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โˆง ๐ด = โˆ…) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)))
63 oveq1 7416 . . . . . . . 8 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (๐ต +o ๐ถ)))
64 oveq1 7416 . . . . . . . . 9 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ (๐ด โ†‘o ๐ต) = (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต))
65 oveq1 7416 . . . . . . . . 9 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ (๐ด โ†‘o ๐ถ) = (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ))
6664, 65oveq12d 7427 . . . . . . . 8 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ)))
6763, 66eqeq12d 2749 . . . . . . 7 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ ((๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)) โ†” (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (๐ต +o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ))))
6867imbi2d 341 . . . . . 6 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ ((๐ถ โˆˆ On โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ))) โ†” (๐ถ โˆˆ On โ†’ (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (๐ต +o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ)))))
69 oveq1 7416 . . . . . . . . 9 (๐ต = if(๐ต โˆˆ On, ๐ต, 1o) โ†’ (๐ต +o ๐ถ) = (if(๐ต โˆˆ On, ๐ต, 1o) +o ๐ถ))
7069oveq2d 7425 . . . . . . . 8 (๐ต = if(๐ต โˆˆ On, ๐ต, 1o) โ†’ (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (๐ต +o ๐ถ)) = (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (if(๐ต โˆˆ On, ๐ต, 1o) +o ๐ถ)))
71 oveq2 7417 . . . . . . . . 9 (๐ต = if(๐ต โˆˆ On, ๐ต, 1o) โ†’ (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต) = (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o if(๐ต โˆˆ On, ๐ต, 1o)))
7271oveq1d 7424 . . . . . . . 8 (๐ต = if(๐ต โˆˆ On, ๐ต, 1o) โ†’ ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o if(๐ต โˆˆ On, ๐ต, 1o)) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ)))
7370, 72eqeq12d 2749 . . . . . . 7 (๐ต = if(๐ต โˆˆ On, ๐ต, 1o) โ†’ ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (๐ต +o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ)) โ†” (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (if(๐ต โˆˆ On, ๐ต, 1o) +o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o if(๐ต โˆˆ On, ๐ต, 1o)) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ))))
7473imbi2d 341 . . . . . 6 (๐ต = if(๐ต โˆˆ On, ๐ต, 1o) โ†’ ((๐ถ โˆˆ On โ†’ (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (๐ต +o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ต) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ))) โ†” (๐ถ โˆˆ On โ†’ (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (if(๐ต โˆˆ On, ๐ต, 1o) +o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o if(๐ต โˆˆ On, ๐ต, 1o)) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ)))))
75 eleq1 2822 . . . . . . . . . 10 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ (๐ด โˆˆ On โ†” if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โˆˆ On))
76 eleq2 2823 . . . . . . . . . 10 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ (โˆ… โˆˆ ๐ด โ†” โˆ… โˆˆ if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o)))
7775, 76anbi12d 632 . . . . . . . . 9 (๐ด = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ ((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด) โ†” (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โˆˆ On โˆง โˆ… โˆˆ if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o))))
78 eleq1 2822 . . . . . . . . . 10 (1o = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ (1o โˆˆ On โ†” if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โˆˆ On))
79 eleq2 2823 . . . . . . . . . 10 (1o = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ (โˆ… โˆˆ 1o โ†” โˆ… โˆˆ if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o)))
8078, 79anbi12d 632 . . . . . . . . 9 (1o = if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†’ ((1o โˆˆ On โˆง โˆ… โˆˆ 1o) โ†” (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โˆˆ On โˆง โˆ… โˆˆ if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o))))
81 1on 8478 . . . . . . . . . 10 1o โˆˆ On
82 0lt1o 8504 . . . . . . . . . 10 โˆ… โˆˆ 1o
8381, 82pm3.2i 472 . . . . . . . . 9 (1o โˆˆ On โˆง โˆ… โˆˆ 1o)
8477, 80, 83elimhyp 4594 . . . . . . . 8 (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โˆˆ On โˆง โˆ… โˆˆ if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o))
8584simpli 485 . . . . . . 7 if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โˆˆ On
8684simpri 487 . . . . . . 7 โˆ… โˆˆ if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o)
8781elimel 4598 . . . . . . 7 if(๐ต โˆˆ On, ๐ต, 1o) โˆˆ On
8885, 86, 87oeoalem 8596 . . . . . 6 (๐ถ โˆˆ On โ†’ (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o (if(๐ต โˆˆ On, ๐ต, 1o) +o ๐ถ)) = ((if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o if(๐ต โˆˆ On, ๐ต, 1o)) ยทo (if((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด), ๐ด, 1o) โ†‘o ๐ถ)))
8968, 74, 88dedth2h 4588 . . . . 5 (((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด) โˆง ๐ต โˆˆ On) โ†’ (๐ถ โˆˆ On โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ))))
9089impr 456 . . . 4 (((๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง ๐ถ โˆˆ On)) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)))
9190an32s 651 . . 3 (((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐ถ โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)))
9262, 91oe0lem 8513 . 2 ((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐ถ โˆˆ On)) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)))
93923impb 1116 1 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (๐ด โ†‘o (๐ต +o ๐ถ)) = ((๐ด โ†‘o ๐ต) ยทo (๐ด โ†‘o ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  โˆ…c0 4323  ifcif 4529  Oncon0 6365  (class class class)co 7409  1oc1o 8459   +o coa 8463   ยทo comu 8464   โ†‘o coe 8465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-omul 8471  df-oexp 8472
This theorem is referenced by:  oeoelem  8598  infxpenc  10013  omabs2  42082
  Copyright terms: Public domain W3C validator