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 42636
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 6417 . . . . 5 (Lim ๐ด โ†’ Ord ๐ด)
2 ordeleqon 7765 . . . . . . 7 (Ord ๐ด โ†” (๐ด โˆˆ On โˆจ ๐ด = On))
32biimpi 215 . . . . . 6 (Ord ๐ด โ†’ (๐ด โˆˆ On โˆจ ๐ด = On))
43orcomd 868 . . . . 5 (Ord ๐ด โ†’ (๐ด = On โˆจ ๐ด โˆˆ On))
51, 4syl 17 . . . 4 (Lim ๐ด โ†’ (๐ด = On โˆจ ๐ด โˆˆ On))
65pm4.71ri 560 . . 3 (Lim ๐ด โ†” ((๐ด = On โˆจ ๐ด โˆˆ On) โˆง Lim ๐ด))
7 andir 1005 . . 3 (((๐ด = On โˆจ ๐ด โˆˆ On) โˆง Lim ๐ด) โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
86, 7bitri 275 . 2 (Lim ๐ด โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
9 limon 7820 . . . . 5 Lim On
10 limeq 6369 . . . . 5 (๐ด = On โ†’ (Lim ๐ด โ†” Lim On))
119, 10mpbiri 258 . . . 4 (๐ด = On โ†’ Lim ๐ด)
1211pm4.71i 559 . . 3 (๐ด = On โ†” (๐ด = On โˆง Lim ๐ด))
1312orbi1i 910 . 2 ((๐ด = On โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)) โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
14 simpl 482 . . . . . 6 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ๐ด โˆˆ On)
15 omelon 9640 . . . . . . . 8 ฯ‰ โˆˆ On
1615a1i 11 . . . . . . 7 (๐ด โˆˆ On โ†’ ฯ‰ โˆˆ On)
17 id 22 . . . . . . 7 (๐ด โˆˆ On โ†’ ๐ด โˆˆ On)
18 peano1 7875 . . . . . . . . 9 โˆ… โˆˆ ฯ‰
1918ne0ii 4332 . . . . . . . 8 ฯ‰ โ‰  โˆ…
2019a1i 11 . . . . . . 7 (๐ด โˆˆ On โ†’ ฯ‰ โ‰  โˆ…)
2116, 17, 203jca 1125 . . . . . 6 (๐ด โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง ๐ด โˆˆ On โˆง ฯ‰ โ‰  โˆ…))
22 omeulem1 8580 . . . . . 6 ((ฯ‰ โˆˆ On โˆง ๐ด โˆˆ On โˆง ฯ‰ โ‰  โˆ…) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
2314, 21, 223syl 18 . . . . 5 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
24 limeq 6369 . . . . . . . . . . . . . . . 16 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim ๐ด))
2524biimprd 247 . . . . . . . . . . . . . . 15 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (Lim ๐ด โ†’ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
26 simplr 766 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ ฯ‰)
27 nnlim 7865 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ ฯ‰ โ†’ ยฌ Lim ๐‘ฆ)
2826, 27syl 17 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ยฌ Lim ๐‘ฆ)
29 on0eln0 6413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฅ โ†” ๐‘ฅ โ‰  โˆ…))
3029biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ โ‰  โˆ… โ†’ โˆ… โˆˆ ๐‘ฅ))
3130necon1bd 2952 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ โˆˆ On โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ๐‘ฅ = โˆ…))
3231adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ๐‘ฅ = โˆ…))
3332imp 406 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ = โˆ…)
3433, 26jca 511 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰))
35 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ฅ = โˆ…)
3635oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) = (ฯ‰ ยทo โˆ…))
37 om0 8515 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ฯ‰ โˆˆ On โ†’ (ฯ‰ ยทo โˆ…) = โˆ…)
3815, 37mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo โˆ…) = โˆ…)
3936, 38eqtrd 2766 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) = โˆ…)
4039oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = (โˆ… +o ๐‘ฆ))
41 nna0r 8607 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ ฯ‰ โ†’ (โˆ… +o ๐‘ฆ) = ๐‘ฆ)
4241adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (โˆ… +o ๐‘ฆ) = ๐‘ฆ)
4340, 42eqtrd 2766 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘ฆ)
44 limeq 6369 . . . . . . . . . . . . . . . . . . . . 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 412 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
48 ovex 7437 . . . . . . . . . . . . . . . . . . . . 21 ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ) โˆˆ V
49 nlimsucg 7827 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ) โˆˆ V โ†’ ยฌ Lim suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
5048, 49mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ยฌ Lim suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
51 nnord 7859 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฆ โˆˆ ฯ‰ โ†’ Ord ๐‘ฆ)
52 orduniorsuc 7814 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Ord ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ))
5351, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ))
54 3ianor 1104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ (Ord ๐‘ฆ โˆง ๐‘ฆ โ‰  โˆ… โˆง ๐‘ฆ = โˆช ๐‘ฆ) โ†” (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
55 df-lim 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim ๐‘ฆ โ†” (Ord ๐‘ฆ โˆง ๐‘ฆ โ‰  โˆ… โˆง ๐‘ฆ = โˆช ๐‘ฆ))
5654, 55xchnxbir 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ยฌ Lim ๐‘ฆ โ†” (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
5727, 56sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
5851pm2.24d 151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ Ord ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
59 nne 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ยฌ ๐‘ฆ โ‰  โˆ… โ†” ๐‘ฆ = โˆ…)
6059biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ ๐‘ฆ โ‰  โˆ… โ†’ ๐‘ฆ = โˆ…)
6160a1i13 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ โ‰  โˆ… โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
62 pm2.21 123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ ๐‘ฆ = โˆช ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…))
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ = โˆช ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
6458, 61, 633jaod 1425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ) โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
6557, 64mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…))
6665orim1d 962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((๐‘ฆ = โˆช ๐‘ฆ โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ) โ†’ (๐‘ฆ = โˆ… โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ)))
6753, 66mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆ… โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ))
6867ord 861 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ))
6968adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ))
7069imp 406 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ)
7170oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ))
72 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ฅ โˆˆ On)
7372adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ๐‘ฅ โˆˆ On)
74 omcl 8534 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
7515, 73, 74sylancr 586 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
76 nnon 7857 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ ฯ‰ โ†’ ๐‘ฆ โˆˆ On)
77 onuni 7772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ On โ†’ โˆช ๐‘ฆ โˆˆ On)
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ ฯ‰ โ†’ โˆช ๐‘ฆ โˆˆ On)
7978adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ โˆช ๐‘ฆ โˆˆ On)
8079adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ โˆช ๐‘ฆ โˆˆ On)
81 oasuc 8522 . . . . . . . . . . . . . . . . . . . . . . 23 (((ฯ‰ ยทo ๐‘ฅ) โˆˆ On โˆง โˆช ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
8275, 80, 81syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
8371, 82eqtrd 2766 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
84 limeq 6369 . . . . . . . . . . . . . . . . . . . . 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 412 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
8847, 87jaod 856 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…) โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
8988con2d 134 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ ยฌ (ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…)))
90 anor 979 . . . . . . . . . . . . . . . 16 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†” ยฌ (ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…))
9189, 90imbitrrdi 251 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)))
9225, 91syl9 77 . . . . . . . . . . . . . 14 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
9392com13 88 . . . . . . . . . . . . 13 (Lim ๐ด โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
9493adantl 481 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
95943imp 1108 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))
96 simp2 1134 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰))
9796, 72syl 17 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ ๐‘ฅ โˆˆ On)
98 simpl 482 . . . . . . . . . . . . . 14 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ โˆ… โˆˆ ๐‘ฅ)
9997, 98anim12i 612 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ (๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ))
100 ondif1 8499 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†” (๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ))
10199, 100sylibr 233 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ๐‘ฅ โˆˆ (On โˆ– 1o))
102 simpr 484 . . . . . . . . . . . . . . 15 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ ๐‘ฆ = โˆ…)
103102oveq2d 7420 . . . . . . . . . . . . . 14 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…))
104103adantl 481 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…))
105 simpl3 1190 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
10615, 72, 74sylancr 586 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
107 oa0 8514 . . . . . . . . . . . . . . 15 ((ฯ‰ ยทo ๐‘ฅ) โˆˆ On โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
10896, 106, 1073syl 18 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
109108adantr 480 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
110104, 105, 1093eqtr3d 2774 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ๐ด = (ฯ‰ ยทo ๐‘ฅ))
111101, 110jca 511 . . . . . . . . . . 11 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))
11295, 111mpdan 684 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))
1131123exp 1116 . . . . . . . . 9 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))))
114113expdimp 452 . . . . . . . 8 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฆ โˆˆ ฯ‰ โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))))
115114rexlimdv 3147 . . . . . . 7 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ))))
116115expimpd 453 . . . . . 6 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ))))
117116reximdv2 3158 . . . . 5 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ (โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
11823, 117mpd 15 . . . 4 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ))
119 simpr 484 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ ๐ด = (ฯ‰ ยทo ๐‘ฅ))
120 eldifi 4121 . . . . . . . . 9 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ ๐‘ฅ โˆˆ On)
12115, 120, 74sylancr 586 . . . . . . . 8 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
122121adantr 480 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
123119, 122eqeltrd 2827 . . . . . 6 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ ๐ด โˆˆ On)
124 limom 7867 . . . . . . . . . . 11 Lim ฯ‰
12515, 124pm3.2i 470 . . . . . . . . . 10 (ฯ‰ โˆˆ On โˆง Lim ฯ‰)
126 omlimcl2 42548 . . . . . . . . . 10 (((๐‘ฅ โˆˆ On โˆง (ฯ‰ โˆˆ On โˆง Lim ฯ‰)) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
127125, 126mpanl2 698 . . . . . . . . 9 ((๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
128100, 127sylbi 216 . . . . . . . 8 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
129128adantr 480 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
130 limeq 6369 . . . . . . . 8 (๐ด = (ฯ‰ ยทo ๐‘ฅ) โ†’ (Lim ๐ด โ†” Lim (ฯ‰ ยทo ๐‘ฅ)))
131130adantl 481 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (Lim ๐ด โ†” Lim (ฯ‰ ยทo ๐‘ฅ)))
132129, 131mpbird 257 . . . . . 6 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ Lim ๐ด)
133123, 132jca 511 . . . . 5 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (๐ด โˆˆ On โˆง Lim ๐ด))
134133rexlimiva 3141 . . . 4 (โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ) โ†’ (๐ด โˆˆ On โˆง Lim ๐ด))
135118, 134impbii 208 . . 3 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†” โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ))
136135orbi2i 909 . 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 395   โˆจ wo 844   โˆจ w3o 1083   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2934  โˆƒwrex 3064  Vcvv 3468   โˆ– cdif 3940  โˆ…c0 4317  โˆช cuni 4902  Ord word 6356  Oncon0 6357  Lim wlim 6358  suc csuc 6359  (class class class)co 7404  ฯ‰com 7851  1oc1o 8457   +o coa 8461   ยทo comu 8462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7721  ax-inf2 9635
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-oadd 8468  df-omul 8469
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator