Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dflim5 Structured version   Visualization version   GIF version

Theorem dflim5 41693
Description: A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025.)
Assertion
Ref Expression
dflim5 (Lim ๐ด โ†” (๐ด = On โˆจ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
Distinct variable group:   ๐‘ฅ,๐ด

Proof of Theorem dflim5
Dummy variable ๐‘ฆ is distinct from all other variables.
StepHypRef Expression
1 limord 6382 . . . . 5 (Lim ๐ด โ†’ Ord ๐ด)
2 ordeleqon 7721 . . . . . . 7 (Ord ๐ด โ†” (๐ด โˆˆ On โˆจ ๐ด = On))
32biimpi 215 . . . . . 6 (Ord ๐ด โ†’ (๐ด โˆˆ On โˆจ ๐ด = On))
43orcomd 870 . . . . 5 (Ord ๐ด โ†’ (๐ด = On โˆจ ๐ด โˆˆ On))
51, 4syl 17 . . . 4 (Lim ๐ด โ†’ (๐ด = On โˆจ ๐ด โˆˆ On))
65pm4.71ri 562 . . 3 (Lim ๐ด โ†” ((๐ด = On โˆจ ๐ด โˆˆ On) โˆง Lim ๐ด))
7 andir 1008 . . 3 (((๐ด = On โˆจ ๐ด โˆˆ On) โˆง Lim ๐ด) โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
86, 7bitri 275 . 2 (Lim ๐ด โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
9 limon 7776 . . . . 5 Lim On
10 limeq 6334 . . . . 5 (๐ด = On โ†’ (Lim ๐ด โ†” Lim On))
119, 10mpbiri 258 . . . 4 (๐ด = On โ†’ Lim ๐ด)
1211pm4.71i 561 . . 3 (๐ด = On โ†” (๐ด = On โˆง Lim ๐ด))
1312orbi1i 913 . 2 ((๐ด = On โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)) โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
14 simpl 484 . . . . . 6 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ๐ด โˆˆ On)
15 omelon 9589 . . . . . . . 8 ฯ‰ โˆˆ On
1615a1i 11 . . . . . . 7 (๐ด โˆˆ On โ†’ ฯ‰ โˆˆ On)
17 id 22 . . . . . . 7 (๐ด โˆˆ On โ†’ ๐ด โˆˆ On)
18 peano1 7830 . . . . . . . . 9 โˆ… โˆˆ ฯ‰
1918ne0ii 4302 . . . . . . . 8 ฯ‰ โ‰  โˆ…
2019a1i 11 . . . . . . 7 (๐ด โˆˆ On โ†’ ฯ‰ โ‰  โˆ…)
2116, 17, 203jca 1129 . . . . . 6 (๐ด โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง ๐ด โˆˆ On โˆง ฯ‰ โ‰  โˆ…))
22 omeulem1 8534 . . . . . 6 ((ฯ‰ โˆˆ On โˆง ๐ด โˆˆ On โˆง ฯ‰ โ‰  โˆ…) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
2314, 21, 223syl 18 . . . . 5 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
24 limeq 6334 . . . . . . . . . . . . . . . 16 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim ๐ด))
2524biimprd 248 . . . . . . . . . . . . . . 15 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (Lim ๐ด โ†’ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
26 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ ฯ‰)
27 nnlim 7821 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ ฯ‰ โ†’ ยฌ Lim ๐‘ฆ)
2826, 27syl 17 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ยฌ Lim ๐‘ฆ)
29 on0eln0 6378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฅ โ†” ๐‘ฅ โ‰  โˆ…))
3029biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ โ‰  โˆ… โ†’ โˆ… โˆˆ ๐‘ฅ))
3130necon1bd 2962 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ โˆˆ On โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ๐‘ฅ = โˆ…))
3231adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ๐‘ฅ = โˆ…))
3332imp 408 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ = โˆ…)
3433, 26jca 513 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰))
35 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ฅ = โˆ…)
3635oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) = (ฯ‰ ยทo โˆ…))
37 om0 8468 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ฯ‰ โˆˆ On โ†’ (ฯ‰ ยทo โˆ…) = โˆ…)
3815, 37mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo โˆ…) = โˆ…)
3936, 38eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) = โˆ…)
4039oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = (โˆ… +o ๐‘ฆ))
41 nna0r 8561 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ ฯ‰ โ†’ (โˆ… +o ๐‘ฆ) = ๐‘ฆ)
4241adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (โˆ… +o ๐‘ฆ) = ๐‘ฆ)
4340, 42eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘ฆ)
44 limeq 6334 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘ฆ โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim ๐‘ฆ))
4534, 43, 443syl 18 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim ๐‘ฆ))
4628, 45mtbird 325 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ))
4746ex 414 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
48 ovex 7395 . . . . . . . . . . . . . . . . . . . . 21 ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ) โˆˆ V
49 nlimsucg 7783 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ) โˆˆ V โ†’ ยฌ Lim suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
5048, 49mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ยฌ Lim suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
51 nnord 7815 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฆ โˆˆ ฯ‰ โ†’ Ord ๐‘ฆ)
52 orduniorsuc 7770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Ord ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ))
5351, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ))
54 3ianor 1108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ (Ord ๐‘ฆ โˆง ๐‘ฆ โ‰  โˆ… โˆง ๐‘ฆ = โˆช ๐‘ฆ) โ†” (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
55 df-lim 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim ๐‘ฆ โ†” (Ord ๐‘ฆ โˆง ๐‘ฆ โ‰  โˆ… โˆง ๐‘ฆ = โˆช ๐‘ฆ))
5654, 55xchnxbir 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ยฌ Lim ๐‘ฆ โ†” (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
5727, 56sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
5851pm2.24d 151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ Ord ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
59 nne 2948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ยฌ ๐‘ฆ โ‰  โˆ… โ†” ๐‘ฆ = โˆ…)
6059biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ ๐‘ฆ โ‰  โˆ… โ†’ ๐‘ฆ = โˆ…)
6160a1i13 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ โ‰  โˆ… โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
62 pm2.21 123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ ๐‘ฆ = โˆช ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…))
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ = โˆช ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
6458, 61, 633jaod 1429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ) โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
6557, 64mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…))
6665orim1d 965 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((๐‘ฆ = โˆช ๐‘ฆ โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ) โ†’ (๐‘ฆ = โˆ… โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ)))
6753, 66mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆ… โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ))
6867ord 863 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ))
6968adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ))
7069imp 408 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ)
7170oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ))
72 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ฅ โˆˆ On)
7372adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ๐‘ฅ โˆˆ On)
74 omcl 8487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
7515, 73, 74sylancr 588 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
76 nnon 7813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ ฯ‰ โ†’ ๐‘ฆ โˆˆ On)
77 onuni 7728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ On โ†’ โˆช ๐‘ฆ โˆˆ On)
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ ฯ‰ โ†’ โˆช ๐‘ฆ โˆˆ On)
7978adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ โˆช ๐‘ฆ โˆˆ On)
8079adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ โˆช ๐‘ฆ โˆˆ On)
81 oasuc 8475 . . . . . . . . . . . . . . . . . . . . . . 23 (((ฯ‰ ยทo ๐‘ฅ) โˆˆ On โˆง โˆช ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
8275, 80, 81syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
8371, 82eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
84 limeq 6334 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ)))
8583, 84syl 17 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ)))
8650, 85mtbird 325 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ))
8786ex 414 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
8847, 87jaod 858 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…) โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
8988con2d 134 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ ยฌ (ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…)))
90 anor 982 . . . . . . . . . . . . . . . 16 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†” ยฌ (ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…))
9189, 90syl6ibr 252 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)))
9225, 91syl9 77 . . . . . . . . . . . . . 14 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
9392com13 88 . . . . . . . . . . . . 13 (Lim ๐ด โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
9493adantl 483 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
95943imp 1112 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))
96 simp2 1138 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰))
9796, 72syl 17 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ ๐‘ฅ โˆˆ On)
98 simpl 484 . . . . . . . . . . . . . 14 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ โˆ… โˆˆ ๐‘ฅ)
9997, 98anim12i 614 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ (๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ))
100 ondif1 8452 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†” (๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ))
10199, 100sylibr 233 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ๐‘ฅ โˆˆ (On โˆ– 1o))
102 simpr 486 . . . . . . . . . . . . . . 15 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ ๐‘ฆ = โˆ…)
103102oveq2d 7378 . . . . . . . . . . . . . 14 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…))
104103adantl 483 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…))
105 simpl3 1194 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
10615, 72, 74sylancr 588 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
107 oa0 8467 . . . . . . . . . . . . . . 15 ((ฯ‰ ยทo ๐‘ฅ) โˆˆ On โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
10896, 106, 1073syl 18 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
109108adantr 482 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
110104, 105, 1093eqtr3d 2785 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ๐ด = (ฯ‰ ยทo ๐‘ฅ))
111101, 110jca 513 . . . . . . . . . . 11 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))
11295, 111mpdan 686 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))
1131123exp 1120 . . . . . . . . 9 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))))
114113expdimp 454 . . . . . . . 8 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฆ โˆˆ ฯ‰ โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))))
115114rexlimdv 3151 . . . . . . 7 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ))))
116115expimpd 455 . . . . . 6 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ))))
117116reximdv2 3162 . . . . 5 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ (โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
11823, 117mpd 15 . . . 4 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ))
119 simpr 486 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ ๐ด = (ฯ‰ ยทo ๐‘ฅ))
120 eldifi 4091 . . . . . . . . 9 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ ๐‘ฅ โˆˆ On)
12115, 120, 74sylancr 588 . . . . . . . 8 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
122121adantr 482 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
123119, 122eqeltrd 2838 . . . . . 6 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ ๐ด โˆˆ On)
124 limom 7823 . . . . . . . . . . 11 Lim ฯ‰
12515, 124pm3.2i 472 . . . . . . . . . 10 (ฯ‰ โˆˆ On โˆง Lim ฯ‰)
126 omlimcl2 41605 . . . . . . . . . 10 (((๐‘ฅ โˆˆ On โˆง (ฯ‰ โˆˆ On โˆง Lim ฯ‰)) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
127125, 126mpanl2 700 . . . . . . . . 9 ((๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
128100, 127sylbi 216 . . . . . . . 8 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
129128adantr 482 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
130 limeq 6334 . . . . . . . 8 (๐ด = (ฯ‰ ยทo ๐‘ฅ) โ†’ (Lim ๐ด โ†” Lim (ฯ‰ ยทo ๐‘ฅ)))
131130adantl 483 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (Lim ๐ด โ†” Lim (ฯ‰ ยทo ๐‘ฅ)))
132129, 131mpbird 257 . . . . . 6 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ Lim ๐ด)
133123, 132jca 513 . . . . 5 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (๐ด โˆˆ On โˆง Lim ๐ด))
134133rexlimiva 3145 . . . 4 (โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ) โ†’ (๐ด โˆˆ On โˆง Lim ๐ด))
135118, 134impbii 208 . . 3 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†” โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ))
136135orbi2i 912 . 2 ((๐ด = On โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)) โ†” (๐ด = On โˆจ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
1378, 13, 1363bitr2i 299 1 (Lim ๐ด โ†” (๐ด = On โˆจ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆจ w3o 1087   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆƒwrex 3074  Vcvv 3448   โˆ– cdif 3912  โˆ…c0 4287  โˆช cuni 4870  Ord word 6321  Oncon0 6322  Lim wlim 6323  suc csuc 6324  (class class class)co 7362  ฯ‰com 7807  1oc1o 8410   +o coa 8414   ยทo comu 8415
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-inf2 9584
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-omul 8422
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator