Metamath Proof Explorer


Theorem omlimcl

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)

Ref Expression
Assertion omlimcl ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ Lim ( ๐ด ยทo ๐ต ) )

Proof

Step Hyp Ref Expression
1 limelon โŠข ( ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) โ†’ ๐ต โˆˆ On )
2 omcl โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ On ) โ†’ ( ๐ด ยทo ๐ต ) โˆˆ On )
3 eloni โŠข ( ( ๐ด ยทo ๐ต ) โˆˆ On โ†’ Ord ( ๐ด ยทo ๐ต ) )
4 2 3 syl โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ On ) โ†’ Ord ( ๐ด ยทo ๐ต ) )
5 1 4 sylan2 โŠข ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โ†’ Ord ( ๐ด ยทo ๐ต ) )
6 5 adantr โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ Ord ( ๐ด ยทo ๐ต ) )
7 0ellim โŠข ( Lim ๐ต โ†’ โˆ… โˆˆ ๐ต )
8 n0i โŠข ( โˆ… โˆˆ ๐ต โ†’ ยฌ ๐ต = โˆ… )
9 7 8 syl โŠข ( Lim ๐ต โ†’ ยฌ ๐ต = โˆ… )
10 n0i โŠข ( โˆ… โˆˆ ๐ด โ†’ ยฌ ๐ด = โˆ… )
11 9 10 anim12ci โŠข ( ( Lim ๐ต โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ… ) )
12 11 adantll โŠข ( ( ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ… ) )
13 12 adantll โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ… ) )
14 om00 โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ On ) โ†’ ( ( ๐ด ยทo ๐ต ) = โˆ… โ†” ( ๐ด = โˆ… โˆจ ๐ต = โˆ… ) ) )
15 14 notbid โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ On ) โ†’ ( ยฌ ( ๐ด ยทo ๐ต ) = โˆ… โ†” ยฌ ( ๐ด = โˆ… โˆจ ๐ต = โˆ… ) ) )
16 ioran โŠข ( ยฌ ( ๐ด = โˆ… โˆจ ๐ต = โˆ… ) โ†” ( ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ… ) )
17 15 16 bitrdi โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ On ) โ†’ ( ยฌ ( ๐ด ยทo ๐ต ) = โˆ… โ†” ( ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ… ) ) )
18 1 17 sylan2 โŠข ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โ†’ ( ยฌ ( ๐ด ยทo ๐ต ) = โˆ… โ†” ( ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ… ) ) )
19 18 adantr โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ยฌ ( ๐ด ยทo ๐ต ) = โˆ… โ†” ( ยฌ ๐ด = โˆ… โˆง ยฌ ๐ต = โˆ… ) ) )
20 13 19 mpbird โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ยฌ ( ๐ด ยทo ๐ต ) = โˆ… )
21 vex โŠข ๐‘ฆ โˆˆ V
22 21 sucid โŠข ๐‘ฆ โˆˆ suc ๐‘ฆ
23 omlim โŠข ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โ†’ ( ๐ด ยทo ๐ต ) = โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) )
24 eqeq1 โŠข ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ( ( ๐ด ยทo ๐ต ) = โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) โ†” suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) ) )
25 24 biimpac โŠข ( ( ( ๐ด ยทo ๐ต ) = โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) โˆง ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†’ suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) )
26 23 25 sylan โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†’ suc ๐‘ฆ = โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) )
27 22 26 eleqtrid โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†’ ๐‘ฆ โˆˆ โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) )
28 eliun โŠข ( ๐‘ฆ โˆˆ โˆช ๐‘ฅ โˆˆ ๐ต ( ๐ด ยทo ๐‘ฅ ) โ†” โˆƒ ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) )
29 27 28 sylib โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†’ โˆƒ ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) )
30 29 adantlr โŠข ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†’ โˆƒ ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) )
31 onelon โŠข ( ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ On )
32 1 31 sylan โŠข ( ( ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ On )
33 onnbtwn โŠข ( ๐‘ฅ โˆˆ On โ†’ ยฌ ( ๐‘ฅ โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐‘ฅ ) )
34 imnan โŠข ( ( ๐‘ฅ โˆˆ ๐ต โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ ) โ†” ยฌ ( ๐‘ฅ โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐‘ฅ ) )
35 33 34 sylibr โŠข ( ๐‘ฅ โˆˆ On โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ ) )
36 35 com12 โŠข ( ๐‘ฅ โˆˆ ๐ต โ†’ ( ๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ ) )
37 36 adantl โŠข ( ( ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ ) )
38 32 37 mpd โŠข ( ( ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ )
39 38 ad5ant24 โŠข ( ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) ) โ†’ ยฌ ๐ต โˆˆ suc ๐‘ฅ )
40 simpl โŠข ( ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ต โˆˆ On )
41 40 31 jca โŠข ( ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) )
42 1 41 sylan โŠข ( ( ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) )
43 42 anim2i โŠข ( ( ๐ด โˆˆ On โˆง ( ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) โˆง ๐‘ฅ โˆˆ ๐ต ) ) โ†’ ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) ) )
44 43 anassrs โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) ) )
45 omcl โŠข ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โ†’ ( ๐ด ยทo ๐‘ฅ ) โˆˆ On )
46 eloni โŠข ( ( ๐ด ยทo ๐‘ฅ ) โˆˆ On โ†’ Ord ( ๐ด ยทo ๐‘ฅ ) )
47 ordsucelsuc โŠข ( Ord ( ๐ด ยทo ๐‘ฅ ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†” suc ๐‘ฆ โˆˆ suc ( ๐ด ยทo ๐‘ฅ ) ) )
48 46 47 syl โŠข ( ( ๐ด ยทo ๐‘ฅ ) โˆˆ On โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†” suc ๐‘ฆ โˆˆ suc ( ๐ด ยทo ๐‘ฅ ) ) )
49 oa1suc โŠข ( ( ๐ด ยทo ๐‘ฅ ) โˆˆ On โ†’ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) = suc ( ๐ด ยทo ๐‘ฅ ) )
50 49 eleq2d โŠข ( ( ๐ด ยทo ๐‘ฅ ) โˆˆ On โ†’ ( suc ๐‘ฆ โˆˆ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โ†” suc ๐‘ฆ โˆˆ suc ( ๐ด ยทo ๐‘ฅ ) ) )
51 48 50 bitr4d โŠข ( ( ๐ด ยทo ๐‘ฅ ) โˆˆ On โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†” suc ๐‘ฆ โˆˆ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) ) )
52 45 51 syl โŠข ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†” suc ๐‘ฆ โˆˆ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) ) )
53 52 adantr โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†” suc ๐‘ฆ โˆˆ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) ) )
54 eloni โŠข ( ๐ด โˆˆ On โ†’ Ord ๐ด )
55 ordgt0ge1 โŠข ( Ord ๐ด โ†’ ( โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด ) )
56 54 55 syl โŠข ( ๐ด โˆˆ On โ†’ ( โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด ) )
57 56 adantr โŠข ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โ†’ ( โˆ… โˆˆ ๐ด โ†” 1o โŠ† ๐ด ) )
58 1on โŠข 1o โˆˆ On
59 oaword โŠข ( ( 1o โˆˆ On โˆง ๐ด โˆˆ On โˆง ( ๐ด ยทo ๐‘ฅ ) โˆˆ On ) โ†’ ( 1o โŠ† ๐ด โ†” ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โŠ† ( ( ๐ด ยทo ๐‘ฅ ) +o ๐ด ) ) )
60 58 59 mp3an1 โŠข ( ( ๐ด โˆˆ On โˆง ( ๐ด ยทo ๐‘ฅ ) โˆˆ On ) โ†’ ( 1o โŠ† ๐ด โ†” ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โŠ† ( ( ๐ด ยทo ๐‘ฅ ) +o ๐ด ) ) )
61 45 60 syldan โŠข ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โ†’ ( 1o โŠ† ๐ด โ†” ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โŠ† ( ( ๐ด ยทo ๐‘ฅ ) +o ๐ด ) ) )
62 57 61 bitrd โŠข ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โ†’ ( โˆ… โˆˆ ๐ด โ†” ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โŠ† ( ( ๐ด ยทo ๐‘ฅ ) +o ๐ด ) ) )
63 62 biimpa โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โŠ† ( ( ๐ด ยทo ๐‘ฅ ) +o ๐ด ) )
64 omsuc โŠข ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โ†’ ( ๐ด ยทo suc ๐‘ฅ ) = ( ( ๐ด ยทo ๐‘ฅ ) +o ๐ด ) )
65 64 adantr โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ๐ด ยทo suc ๐‘ฅ ) = ( ( ๐ด ยทo ๐‘ฅ ) +o ๐ด ) )
66 63 65 sseqtrrd โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โŠ† ( ๐ด ยทo suc ๐‘ฅ ) )
67 66 sseld โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( suc ๐‘ฆ โˆˆ ( ( ๐ด ยทo ๐‘ฅ ) +o 1o ) โ†’ suc ๐‘ฆ โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) )
68 53 67 sylbid โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ suc ๐‘ฆ โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) )
69 eleq1 โŠข ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ( ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) โ†” suc ๐‘ฆ โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) )
70 69 biimprd โŠข ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ( suc ๐‘ฆ โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) โ†’ ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) )
71 68 70 syl9 โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) ) )
72 71 com23 โŠข ( ( ( ๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) ) )
73 72 adantlrl โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) ) )
74 sucelon โŠข ( ๐‘ฅ โˆˆ On โ†” suc ๐‘ฅ โˆˆ On )
75 omord โŠข ( ( ๐ต โˆˆ On โˆง suc ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On ) โ†’ ( ( ๐ต โˆˆ suc ๐‘ฅ โˆง โˆ… โˆˆ ๐ด ) โ†” ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) ) )
76 simpl โŠข ( ( ๐ต โˆˆ suc ๐‘ฅ โˆง โˆ… โˆˆ ๐ด ) โ†’ ๐ต โˆˆ suc ๐‘ฅ )
77 75 76 syl6bir โŠข ( ( ๐ต โˆˆ On โˆง suc ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On ) โ†’ ( ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) โ†’ ๐ต โˆˆ suc ๐‘ฅ ) )
78 74 77 syl3an2b โŠข ( ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On ) โ†’ ( ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) โ†’ ๐ต โˆˆ suc ๐‘ฅ ) )
79 78 3comr โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) โ†’ ( ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) โ†’ ๐ต โˆˆ suc ๐‘ฅ ) )
80 79 3expb โŠข ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) ) โ†’ ( ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) โ†’ ๐ต โˆˆ suc ๐‘ฅ ) )
81 80 adantr โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ( ๐ด ยทo ๐ต ) โˆˆ ( ๐ด ยทo suc ๐‘ฅ ) โ†’ ๐ต โˆˆ suc ๐‘ฅ ) )
82 73 81 syl6d โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ ) ) )
83 44 82 sylan โŠข ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ ) ) )
84 83 an32s โŠข ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ ) ) )
85 84 imp โŠข ( ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) ) โ†’ ( ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ โ†’ ๐ต โˆˆ suc ๐‘ฅ ) )
86 39 85 mtod โŠข ( ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) ) โ†’ ยฌ ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ )
87 86 rexlimdva2 โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( โˆƒ ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ยฌ ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) )
88 87 adantr โŠข ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†’ ( โˆƒ ๐‘ฅ โˆˆ ๐ต ๐‘ฆ โˆˆ ( ๐ด ยทo ๐‘ฅ ) โ†’ ยฌ ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) )
89 30 88 mpd โŠข ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†’ ยฌ ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ )
90 89 pm2.01da โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ยฌ ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ )
91 90 adantr โŠข ( ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โˆง ๐‘ฆ โˆˆ On ) โ†’ ยฌ ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ )
92 91 nrexdv โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ยฌ โˆƒ ๐‘ฆ โˆˆ On ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ )
93 ioran โŠข ( ยฌ ( ( ๐ด ยทo ๐ต ) = โˆ… โˆจ โˆƒ ๐‘ฆ โˆˆ On ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) โ†” ( ยฌ ( ๐ด ยทo ๐ต ) = โˆ… โˆง ยฌ โˆƒ ๐‘ฆ โˆˆ On ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) )
94 20 92 93 sylanbrc โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ยฌ ( ( ๐ด ยทo ๐ต ) = โˆ… โˆจ โˆƒ ๐‘ฆ โˆˆ On ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) )
95 dflim3 โŠข ( Lim ( ๐ด ยทo ๐ต ) โ†” ( Ord ( ๐ด ยทo ๐ต ) โˆง ยฌ ( ( ๐ด ยทo ๐ต ) = โˆ… โˆจ โˆƒ ๐‘ฆ โˆˆ On ( ๐ด ยทo ๐ต ) = suc ๐‘ฆ ) ) )
96 6 94 95 sylanbrc โŠข ( ( ( ๐ด โˆˆ On โˆง ( ๐ต โˆˆ ๐ถ โˆง Lim ๐ต ) ) โˆง โˆ… โˆˆ ๐ด ) โ†’ Lim ( ๐ด ยทo ๐ต ) )