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

Theorem omlimcl 8577
Description: The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of [TakeutiZaring] p. 64. (Contributed by NM, 25-Dec-2004.)
Assertion
Ref Expression
omlimcl (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ Lim (๐ด ยทo ๐ต))

Proof of Theorem omlimcl
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limelon 6428 . . . 4 ((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โ†’ ๐ต โˆˆ On)
2 omcl 8535 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
3 eloni 6374 . . . . 5 ((๐ด ยทo ๐ต) โˆˆ On โ†’ Ord (๐ด ยทo ๐ต))
42, 3syl 17 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ Ord (๐ด ยทo ๐ต))
51, 4sylan2 593 . . 3 ((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โ†’ Ord (๐ด ยทo ๐ต))
65adantr 481 . 2 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ Ord (๐ด ยทo ๐ต))
7 0ellim 6427 . . . . . . . 8 (Lim ๐ต โ†’ โˆ… โˆˆ ๐ต)
8 n0i 4333 . . . . . . . 8 (โˆ… โˆˆ ๐ต โ†’ ยฌ ๐ต = โˆ…)
97, 8syl 17 . . . . . . 7 (Lim ๐ต โ†’ ยฌ ๐ต = โˆ…)
10 n0i 4333 . . . . . . 7 (โˆ… โˆˆ ๐ด โ†’ ยฌ ๐ด = โˆ…)
119, 10anim12ci 614 . . . . . 6 ((Lim ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
1211adantll 712 . . . . 5 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
1312adantll 712 . . . 4 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
14 om00 8574 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) = โˆ… โ†” (๐ด = โˆ… โˆจ ๐ต = โˆ…)))
1514notbid 317 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” ยฌ (๐ด = โˆ… โˆจ ๐ต = โˆ…)))
16 ioran 982 . . . . . . 7 (ยฌ (๐ด = โˆ… โˆจ ๐ต = โˆ…) โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
1715, 16bitrdi 286 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…)))
181, 17sylan2 593 . . . . 5 ((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…)))
1918adantr 481 . . . 4 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…)))
2013, 19mpbird 256 . . 3 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ (๐ด ยทo ๐ต) = โˆ…)
21 vex 3478 . . . . . . . . . . 11 ๐‘ฆ โˆˆ V
2221sucid 6446 . . . . . . . . . 10 ๐‘ฆ โˆˆ suc ๐‘ฆ
23 omlim 8532 . . . . . . . . . . 11 ((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โ†’ (๐ด ยทo ๐ต) = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
24 eqeq1 2736 . . . . . . . . . . . 12 ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ)))
2524biimpac 479 . . . . . . . . . . 11 (((๐ด ยทo ๐ต) = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
2623, 25sylan 580 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
2722, 26eleqtrid 2839 . . . . . . . . 9 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ ๐‘ฆ โˆˆ โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
28 eliun 5001 . . . . . . . . 9 (๐‘ฆ โˆˆ โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ) โ†” โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ))
2927, 28sylib 217 . . . . . . . 8 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ))
3029adantlr 713 . . . . . . 7 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ))
31 onelon 6389 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
321, 31sylan 580 . . . . . . . . . . . 12 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
33 onnbtwn 6458 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ On โ†’ ยฌ (๐‘ฅ โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐‘ฅ))
34 imnan 400 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ ๐ต โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ) โ†” ยฌ (๐‘ฅ โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐‘ฅ))
3533, 34sylibr 233 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ))
3635com12 32 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ ๐ต โ†’ (๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ))
3736adantl 482 . . . . . . . . . . . 12 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ))
3832, 37mpd 15 . . . . . . . . . . 11 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ)
3938ad5ant24 759 . . . . . . . . . 10 (((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ)) โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ)
40 simpl 483 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐ต โˆˆ On)
4140, 31jca 512 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On))
421, 41sylan 580 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On))
4342anim2i 617 . . . . . . . . . . . . . 14 ((๐ด โˆˆ On โˆง ((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต)) โ†’ (๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)))
4443anassrs 468 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)))
45 omcl 8535 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
46 eloni 6374 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ Ord (๐ด ยทo ๐‘ฅ))
47 ordsucelsuc 7809 . . . . . . . . . . . . . . . . . . . . . 22 (Ord (๐ด ยทo ๐‘ฅ) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ suc (๐ด ยทo ๐‘ฅ)))
4846, 47syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ suc (๐ด ยทo ๐‘ฅ)))
49 oa1suc 8530 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ ((๐ด ยทo ๐‘ฅ) +o 1o) = suc (๐ด ยทo ๐‘ฅ))
5049eleq2d 2819 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ (suc ๐‘ฆ โˆˆ ((๐ด ยทo ๐‘ฅ) +o 1o) โ†” suc ๐‘ฆ โˆˆ suc (๐ด ยทo ๐‘ฅ)))
5148, 50bitr4d 281 . . . . . . . . . . . . . . . . . . . 20 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ ((๐ด ยทo ๐‘ฅ) +o 1o)))
5245, 51syl 17 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ ((๐ด ยทo ๐‘ฅ) +o 1o)))
5352adantr 481 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ ((๐ด ยทo ๐‘ฅ) +o 1o)))
54 eloni 6374 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ด โˆˆ On โ†’ Ord ๐ด)
55 ordgt0ge1 8492 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord ๐ด โ†’ (โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด))
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด))
5756adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด))
58 1on 8477 . . . . . . . . . . . . . . . . . . . . . . . 24 1o โˆˆ On
59 oaword 8548 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1o โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (1o โŠ† ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6058, 59mp3an1 1448 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (1o โŠ† ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6145, 60syldan 591 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (1o โŠ† ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6257, 61bitrd 278 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6362biimpa 477 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด))
64 omsuc 8525 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
6564adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
6663, 65sseqtrrd 4023 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† (๐ด ยทo suc ๐‘ฅ))
6766sseld 3981 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (suc ๐‘ฆ โˆˆ ((๐ด ยทo ๐‘ฅ) +o 1o) โ†’ suc ๐‘ฆ โˆˆ (๐ด ยทo suc ๐‘ฅ)))
6853, 67sylbid 239 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ suc ๐‘ฆ โˆˆ (๐ด ยทo suc ๐‘ฅ)))
69 eleq1 2821 . . . . . . . . . . . . . . . . . 18 ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ (๐ด ยทo suc ๐‘ฅ)))
7069biimprd 247 . . . . . . . . . . . . . . . . 17 ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ (suc ๐‘ฆ โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ)))
7168, 70syl9 77 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ))))
7271com23 86 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ))))
7372adantlrl 718 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ))))
74 onsucb 7804 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ On โ†” suc ๐‘ฅ โˆˆ On)
75 omord 8567 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ On โˆง suc ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ ((๐ต โˆˆ suc ๐‘ฅ โˆง โˆ… โˆˆ ๐ด) โ†” (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ)))
76 simpl 483 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ suc ๐‘ฅ โˆง โˆ… โˆˆ ๐ด) โ†’ ๐ต โˆˆ suc ๐‘ฅ)
7775, 76syl6bir 253 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ On โˆง suc ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
7874, 77syl3an2b 1404 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
79783comr 1125 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
80793expb 1120 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
8180adantr 481 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
8273, 81syl6d 75 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ)))
8344, 82sylan 580 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ)))
8483an32s 650 . . . . . . . . . . 11 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ)))
8584imp 407 . . . . . . . . . 10 (((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ)) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ))
8639, 85mtod 197 . . . . . . . . 9 (((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ)) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
8786rexlimdva2 3157 . . . . . . . 8 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ))
8887adantr 481 . . . . . . 7 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ))
8930, 88mpd 15 . . . . . 6 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
9089pm2.01da 797 . . . . 5 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
9190adantr 481 . . . 4 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฆ โˆˆ On) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
9291nrexdv 3149 . . 3 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ)
93 ioran 982 . . 3 (ยฌ ((๐ด ยทo ๐ต) = โˆ… โˆจ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†” (ยฌ (๐ด ยทo ๐ต) = โˆ… โˆง ยฌ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ))
9420, 92, 93sylanbrc 583 . 2 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ ((๐ด ยทo ๐ต) = โˆ… โˆจ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ))
95 dflim3 7835 . 2 (Lim (๐ด ยทo ๐ต) โ†” (Ord (๐ด ยทo ๐ต) โˆง ยฌ ((๐ด ยทo ๐ต) = โˆ… โˆจ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ)))
966, 94, 95sylanbrc 583 1 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ Lim (๐ด ยทo ๐ต))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106  โˆƒwrex 3070   โŠ† wss 3948  โˆ…c0 4322  โˆช ciun 4997  Ord word 6363  Oncon0 6364  Lim wlim 6365  suc csuc 6366  (class class class)co 7408  1oc1o 8458   +o coa 8462   ยทo comu 8463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-oadd 8469  df-omul 8470
This theorem is referenced by:  odi  8578  omass  8579  omlimcl2  41981  omlim2  42039
  Copyright terms: Public domain W3C validator