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

Theorem omlimcl 8580
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 6427 . . . 4 ((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โ†’ ๐ต โˆˆ On)
2 omcl 8538 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
3 eloni 6373 . . . . 5 ((๐ด ยทo ๐ต) โˆˆ On โ†’ Ord (๐ด ยทo ๐ต))
42, 3syl 17 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ Ord (๐ด ยทo ๐ต))
51, 4sylan2 591 . . 3 ((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โ†’ Ord (๐ด ยทo ๐ต))
65adantr 479 . 2 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ Ord (๐ด ยทo ๐ต))
7 0ellim 6426 . . . . . . . 8 (Lim ๐ต โ†’ โˆ… โˆˆ ๐ต)
8 n0i 4332 . . . . . . . 8 (โˆ… โˆˆ ๐ต โ†’ ยฌ ๐ต = โˆ…)
97, 8syl 17 . . . . . . 7 (Lim ๐ต โ†’ ยฌ ๐ต = โˆ…)
10 n0i 4332 . . . . . . 7 (โˆ… โˆˆ ๐ด โ†’ ยฌ ๐ด = โˆ…)
119, 10anim12ci 612 . . . . . 6 ((Lim ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
1211adantll 710 . . . . 5 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
1312adantll 710 . . . 4 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
14 om00 8577 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) = โˆ… โ†” (๐ด = โˆ… โˆจ ๐ต = โˆ…)))
1514notbid 317 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” ยฌ (๐ด = โˆ… โˆจ ๐ต = โˆ…)))
16 ioran 980 . . . . . . 7 (ยฌ (๐ด = โˆ… โˆจ ๐ต = โˆ…) โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…))
1715, 16bitrdi 286 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…)))
181, 17sylan2 591 . . . . 5 ((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…)))
1918adantr 479 . . . 4 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ (ยฌ (๐ด ยทo ๐ต) = โˆ… โ†” (ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ…)))
2013, 19mpbird 256 . . 3 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ (๐ด ยทo ๐ต) = โˆ…)
21 vex 3476 . . . . . . . . . . 11 ๐‘ฆ โˆˆ V
2221sucid 6445 . . . . . . . . . 10 ๐‘ฆ โˆˆ suc ๐‘ฆ
23 omlim 8535 . . . . . . . . . . 11 ((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โ†’ (๐ด ยทo ๐ต) = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
24 eqeq1 2734 . . . . . . . . . . . 12 ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ)))
2524biimpac 477 . . . . . . . . . . 11 (((๐ด ยทo ๐ต) = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
2623, 25sylan 578 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
2722, 26eleqtrid 2837 . . . . . . . . 9 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ ๐‘ฆ โˆˆ โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ))
28 eliun 5000 . . . . . . . . 9 (๐‘ฆ โˆˆ โˆช ๐‘ฅ โˆˆ ๐ต (๐ด ยทo ๐‘ฅ) โ†” โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ))
2927, 28sylib 217 . . . . . . . 8 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ))
3029adantlr 711 . . . . . . 7 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ))
31 onelon 6388 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
321, 31sylan 578 . . . . . . . . . . . 12 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
33 onnbtwn 6457 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ On โ†’ ยฌ (๐‘ฅ โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐‘ฅ))
34 imnan 398 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ ๐ต โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ) โ†” ยฌ (๐‘ฅ โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐‘ฅ))
3533, 34sylibr 233 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ))
3635com12 32 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ ๐ต โ†’ (๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ))
3736adantl 480 . . . . . . . . . . . 12 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ))
3832, 37mpd 15 . . . . . . . . . . 11 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ)
3938ad5ant24 757 . . . . . . . . . 10 (((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ)) โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ)
40 simpl 481 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐ต โˆˆ On)
4140, 31jca 510 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On))
421, 41sylan 578 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On))
4342anim2i 615 . . . . . . . . . . . . . 14 ((๐ด โˆˆ On โˆง ((๐ต โˆˆ ๐ถ โˆง Lim ๐ต) โˆง ๐‘ฅ โˆˆ ๐ต)) โ†’ (๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)))
4443anassrs 466 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)))
45 omcl 8538 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
46 eloni 6373 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ Ord (๐ด ยทo ๐‘ฅ))
47 ordsucelsuc 7812 . . . . . . . . . . . . . . . . . . . . . 22 (Ord (๐ด ยทo ๐‘ฅ) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ suc (๐ด ยทo ๐‘ฅ)))
4846, 47syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ suc (๐ด ยทo ๐‘ฅ)))
49 oa1suc 8533 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด ยทo ๐‘ฅ) โˆˆ On โ†’ ((๐ด ยทo ๐‘ฅ) +o 1o) = suc (๐ด ยทo ๐‘ฅ))
5049eleq2d 2817 . . . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†” suc ๐‘ฆ โˆˆ ((๐ด ยทo ๐‘ฅ) +o 1o)))
54 eloni 6373 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ด โˆˆ On โ†’ Ord ๐ด)
55 ordgt0ge1 8495 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord ๐ด โ†’ (โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด))
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด))
5756adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด))
58 1on 8480 . . . . . . . . . . . . . . . . . . . . . . . 24 1o โˆˆ On
59 oaword 8551 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1o โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (1o โŠ† ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6058, 59mp3an1 1446 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (1o โŠ† ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6145, 60syldan 589 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (1o โŠ† ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6257, 61bitrd 278 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
6362biimpa 475 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐ด))
64 omsuc 8528 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
6564adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
6663, 65sseqtrrd 4022 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐‘ฅ) +o 1o) โŠ† (๐ด ยทo suc ๐‘ฅ))
6766sseld 3980 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (suc ๐‘ฆ โˆˆ ((๐ด ยทo ๐‘ฅ) +o 1o) โ†’ suc ๐‘ฆ โˆˆ (๐ด ยทo suc ๐‘ฅ)))
6853, 67sylbid 239 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ suc ๐‘ฆ โˆˆ (๐ด ยทo suc ๐‘ฅ)))
69 eleq1 2819 . . . . . . . . . . . . . . . . . 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 716 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ))))
74 onsucb 7807 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ On โ†” suc ๐‘ฅ โˆˆ On)
75 omord 8570 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ On โˆง suc ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ ((๐ต โˆˆ suc ๐‘ฅ โˆง โˆ… โˆˆ ๐ด) โ†” (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ)))
76 simpl 481 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ suc ๐‘ฅ โˆง โˆ… โˆˆ ๐ด) โ†’ ๐ต โˆˆ suc ๐‘ฅ)
7775, 76syl6bir 253 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ On โˆง suc ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
7874, 77syl3an2b 1402 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
79783comr 1123 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
80793expb 1118 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
8180adantr 479 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐ต) โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ ๐ต โˆˆ suc ๐‘ฅ))
8273, 81syl6d 75 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ)))
8344, 82sylan 578 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ)))
8483an32s 648 . . . . . . . . . . 11 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ)))
8584imp 405 . . . . . . . . . 10 (((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ)) โ†’ ((๐ด ยทo ๐ต) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ))
8639, 85mtod 197 . . . . . . . . 9 (((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ)) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
8786rexlimdva2 3155 . . . . . . . 8 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ))
8887adantr 479 . . . . . . 7 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ))
8930, 88mpd 15 . . . . . 6 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
9089pm2.01da 795 . . . . 5 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
9190adantr 479 . . . 4 ((((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โˆง ๐‘ฆ โˆˆ On) โ†’ ยฌ (๐ด ยทo ๐ต) = suc ๐‘ฆ)
9291nrexdv 3147 . . 3 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ)
93 ioran 980 . . 3 (ยฌ ((๐ด ยทo ๐ต) = โˆ… โˆจ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ) โ†” (ยฌ (๐ด ยทo ๐ต) = โˆ… โˆง ยฌ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ))
9420, 92, 93sylanbrc 581 . 2 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ ยฌ ((๐ด ยทo ๐ต) = โˆ… โˆจ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ))
95 dflim3 7838 . 2 (Lim (๐ด ยทo ๐ต) โ†” (Ord (๐ด ยทo ๐ต) โˆง ยฌ ((๐ด ยทo ๐ต) = โˆ… โˆจ โˆƒ๐‘ฆ โˆˆ On (๐ด ยทo ๐ต) = suc ๐‘ฆ)))
966, 94, 95sylanbrc 581 1 (((๐ด โˆˆ On โˆง (๐ต โˆˆ ๐ถ โˆง Lim ๐ต)) โˆง โˆ… โˆˆ ๐ด) โ†’ Lim (๐ด ยทo ๐ต))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 843   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104  โˆƒwrex 3068   โŠ† wss 3947  โˆ…c0 4321  โˆช ciun 4996  Ord word 6362  Oncon0 6363  Lim wlim 6364  suc csuc 6365  (class class class)co 7411  1oc1o 8461   +o coa 8465   ยทo comu 8466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-omul 8473
This theorem is referenced by:  odi  8581  omass  8582  omlimcl2  42293  omlim2  42351
  Copyright terms: Public domain W3C validator