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 42064
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 6421 . . . . 5 (Lim ๐ด โ†’ Ord ๐ด)
2 ordeleqon 7765 . . . . . . 7 (Ord ๐ด โ†” (๐ด โˆˆ On โˆจ ๐ด = On))
32biimpi 215 . . . . . 6 (Ord ๐ด โ†’ (๐ด โˆˆ On โˆจ ๐ด = On))
43orcomd 869 . . . . 5 (Ord ๐ด โ†’ (๐ด = On โˆจ ๐ด โˆˆ On))
51, 4syl 17 . . . 4 (Lim ๐ด โ†’ (๐ด = On โˆจ ๐ด โˆˆ On))
65pm4.71ri 561 . . 3 (Lim ๐ด โ†” ((๐ด = On โˆจ ๐ด โˆˆ On) โˆง Lim ๐ด))
7 andir 1007 . . 3 (((๐ด = On โˆจ ๐ด โˆˆ On) โˆง Lim ๐ด) โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
86, 7bitri 274 . 2 (Lim ๐ด โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
9 limon 7820 . . . . 5 Lim On
10 limeq 6373 . . . . 5 (๐ด = On โ†’ (Lim ๐ด โ†” Lim On))
119, 10mpbiri 257 . . . 4 (๐ด = On โ†’ Lim ๐ด)
1211pm4.71i 560 . . 3 (๐ด = On โ†” (๐ด = On โˆง Lim ๐ด))
1312orbi1i 912 . 2 ((๐ด = On โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)) โ†” ((๐ด = On โˆง Lim ๐ด) โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)))
14 simpl 483 . . . . . 6 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ๐ด โˆˆ On)
15 omelon 9637 . . . . . . . 8 ฯ‰ โˆˆ On
1615a1i 11 . . . . . . 7 (๐ด โˆˆ On โ†’ ฯ‰ โˆˆ On)
17 id 22 . . . . . . 7 (๐ด โˆˆ On โ†’ ๐ด โˆˆ On)
18 peano1 7875 . . . . . . . . 9 โˆ… โˆˆ ฯ‰
1918ne0ii 4336 . . . . . . . 8 ฯ‰ โ‰  โˆ…
2019a1i 11 . . . . . . 7 (๐ด โˆˆ On โ†’ ฯ‰ โ‰  โˆ…)
2116, 17, 203jca 1128 . . . . . 6 (๐ด โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง ๐ด โˆˆ On โˆง ฯ‰ โ‰  โˆ…))
22 omeulem1 8578 . . . . . 6 ((ฯ‰ โˆˆ On โˆง ๐ด โˆˆ On โˆง ฯ‰ โ‰  โˆ…) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
2314, 21, 223syl 18 . . . . 5 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
24 limeq 6373 . . . . . . . . . . . . . . . 16 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim ๐ด))
2524biimprd 247 . . . . . . . . . . . . . . 15 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (Lim ๐ด โ†’ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
26 simplr 767 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ ฯ‰)
27 nnlim 7865 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ ฯ‰ โ†’ ยฌ Lim ๐‘ฆ)
2826, 27syl 17 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ยฌ Lim ๐‘ฆ)
29 on0eln0 6417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฅ โ†” ๐‘ฅ โ‰  โˆ…))
3029biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ โ‰  โˆ… โ†’ โˆ… โˆˆ ๐‘ฅ))
3130necon1bd 2958 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ โˆˆ On โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ๐‘ฅ = โˆ…))
3231adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ๐‘ฅ = โˆ…))
3332imp 407 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ = โˆ…)
3433, 26jca 512 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰))
35 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ฅ = โˆ…)
3635oveq2d 7421 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) = (ฯ‰ ยทo โˆ…))
37 om0 8513 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ฯ‰ โˆˆ On โ†’ (ฯ‰ ยทo โˆ…) = โˆ…)
3815, 37mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo โˆ…) = โˆ…)
3936, 38eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) = โˆ…)
4039oveq1d 7420 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = (โˆ… +o ๐‘ฆ))
41 nna0r 8605 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ ฯ‰ โ†’ (โˆ… +o ๐‘ฆ) = ๐‘ฆ)
4241adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (โˆ… +o ๐‘ฆ) = ๐‘ฆ)
4340, 42eqtrd 2772 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ = โˆ… โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘ฆ)
44 limeq 6373 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘ฆ โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim ๐‘ฆ))
4534, 43, 443syl 18 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” Lim ๐‘ฆ))
4628, 45mtbird 324 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ โˆ… โˆˆ ๐‘ฅ) โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ))
4746ex 413 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ โˆ… โˆˆ ๐‘ฅ โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
48 ovex 7438 . . . . . . . . . . . . . . . . . . . . 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 1107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ (Ord ๐‘ฆ โˆง ๐‘ฆ โ‰  โˆ… โˆง ๐‘ฆ = โˆช ๐‘ฆ) โ†” (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
55 df-lim 6366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim ๐‘ฆ โ†” (Ord ๐‘ฆ โˆง ๐‘ฆ โ‰  โˆ… โˆง ๐‘ฆ = โˆช ๐‘ฆ))
5654, 55xchnxbir 332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ยฌ Lim ๐‘ฆ โ†” (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
5727, 56sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ))
5851pm2.24d 151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ Ord ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
59 nne 2944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ยฌ ๐‘ฆ โ‰  โˆ… โ†” ๐‘ฆ = โˆ…)
6059biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ ๐‘ฆ โ‰  โˆ… โ†’ ๐‘ฆ = โˆ…)
6160a1i13 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ โ‰  โˆ… โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
62 pm2.21 123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ยฌ ๐‘ฆ = โˆช ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…))
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ = โˆช ๐‘ฆ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
6458, 61, 633jaod 1428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((ยฌ Ord ๐‘ฆ โˆจ ยฌ ๐‘ฆ โ‰  โˆ… โˆจ ยฌ ๐‘ฆ = โˆช ๐‘ฆ) โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…)))
6557, 64mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆช ๐‘ฆ โ†’ ๐‘ฆ = โˆ…))
6665orim1d 964 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((๐‘ฆ = โˆช ๐‘ฆ โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ) โ†’ (๐‘ฆ = โˆ… โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ)))
6753, 66mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ = โˆ… โˆจ ๐‘ฆ = suc โˆช ๐‘ฆ))
6867ord 862 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ ฯ‰ โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ))
6968adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ))
7069imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ๐‘ฆ = suc โˆช ๐‘ฆ)
7170oveq2d 7421 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ))
72 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ฅ โˆˆ On)
7372adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ๐‘ฅ โˆˆ On)
74 omcl 8532 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
7515, 73, 74sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
76 nnon 7857 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ ฯ‰ โ†’ ๐‘ฆ โˆˆ On)
77 onuni 7772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ On โ†’ โˆช ๐‘ฆ โˆˆ On)
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ ฯ‰ โ†’ โˆช ๐‘ฆ โˆˆ On)
7978adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ โˆช ๐‘ฆ โˆˆ On)
8079adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ โˆช ๐‘ฆ โˆˆ On)
81 oasuc 8520 . . . . . . . . . . . . . . . . . . . . . . 23 (((ฯ‰ ยทo ๐‘ฅ) โˆˆ On โˆง โˆช ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
8275, 80, 81syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o suc โˆช ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
8371, 82eqtrd 2772 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = suc ((ฯ‰ ยทo ๐‘ฅ) +o โˆช ๐‘ฆ))
84 limeq 6373 . . . . . . . . . . . . . . . . . . . . 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 324 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ยฌ ๐‘ฆ = โˆ…) โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ))
8786ex 413 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ยฌ ๐‘ฆ = โˆ… โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
8847, 87jaod 857 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…) โ†’ ยฌ Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ)))
8988con2d 134 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ ยฌ (ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…)))
90 anor 981 . . . . . . . . . . . . . . . 16 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†” ยฌ (ยฌ โˆ… โˆˆ ๐‘ฅ โˆจ ยฌ ๐‘ฆ = โˆ…))
9189, 90syl6ibr 251 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)))
9225, 91syl9 77 . . . . . . . . . . . . . 14 (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (Lim ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
9392com13 88 . . . . . . . . . . . . 13 (Lim ๐ด โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
9493adantl 482 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))))
95943imp 1111 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…))
96 simp2 1137 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰))
9796, 72syl 17 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ ๐‘ฅ โˆˆ On)
98 simpl 483 . . . . . . . . . . . . . 14 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ โˆ… โˆˆ ๐‘ฅ)
9997, 98anim12i 613 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ (๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ))
100 ondif1 8497 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†” (๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ))
10199, 100sylibr 233 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ๐‘ฅ โˆˆ (On โˆ– 1o))
102 simpr 485 . . . . . . . . . . . . . . 15 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ ๐‘ฆ = โˆ…)
103102oveq2d 7421 . . . . . . . . . . . . . 14 ((โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…))
104103adantl 482 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…))
105 simpl3 1193 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด)
10615, 72, 74sylancr 587 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
107 oa0 8512 . . . . . . . . . . . . . . 15 ((ฯ‰ ยทo ๐‘ฅ) โˆˆ On โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
10896, 106, 1073syl 18 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
109108adantr 481 . . . . . . . . . . . . 13 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ((ฯ‰ ยทo ๐‘ฅ) +o โˆ…) = (ฯ‰ ยทo ๐‘ฅ))
110104, 105, 1093eqtr3d 2780 . . . . . . . . . . . 12 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ ๐ด = (ฯ‰ ยทo ๐‘ฅ))
111101, 110jca 512 . . . . . . . . . . 11 ((((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โˆง (โˆ… โˆˆ ๐‘ฅ โˆง ๐‘ฆ = โˆ…)) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))
11295, 111mpdan 685 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))
1131123exp 1119 . . . . . . . . 9 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))))
114113expdimp 453 . . . . . . . 8 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฆ โˆˆ ฯ‰ โ†’ (((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)))))
115114rexlimdv 3153 . . . . . . 7 (((๐ด โˆˆ On โˆง Lim ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ))))
116115expimpd 454 . . . . . 6 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ ((๐‘ฅ โˆˆ On โˆง โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด) โ†’ (๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ))))
117116reximdv2 3164 . . . . 5 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ (โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ฯ‰ ((ฯ‰ ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
11823, 117mpd 15 . . . 4 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ))
119 simpr 485 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ ๐ด = (ฯ‰ ยทo ๐‘ฅ))
120 eldifi 4125 . . . . . . . . 9 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ ๐‘ฅ โˆˆ On)
12115, 120, 74sylancr 587 . . . . . . . 8 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
122121adantr 481 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (ฯ‰ ยทo ๐‘ฅ) โˆˆ On)
123119, 122eqeltrd 2833 . . . . . 6 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ ๐ด โˆˆ On)
124 limom 7867 . . . . . . . . . . 11 Lim ฯ‰
12515, 124pm3.2i 471 . . . . . . . . . 10 (ฯ‰ โˆˆ On โˆง Lim ฯ‰)
126 omlimcl2 41976 . . . . . . . . . 10 (((๐‘ฅ โˆˆ On โˆง (ฯ‰ โˆˆ On โˆง Lim ฯ‰)) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
127125, 126mpanl2 699 . . . . . . . . 9 ((๐‘ฅ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
128100, 127sylbi 216 . . . . . . . 8 (๐‘ฅ โˆˆ (On โˆ– 1o) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
129128adantr 481 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ Lim (ฯ‰ ยทo ๐‘ฅ))
130 limeq 6373 . . . . . . . 8 (๐ด = (ฯ‰ ยทo ๐‘ฅ) โ†’ (Lim ๐ด โ†” Lim (ฯ‰ ยทo ๐‘ฅ)))
131130adantl 482 . . . . . . 7 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (Lim ๐ด โ†” Lim (ฯ‰ ยทo ๐‘ฅ)))
132129, 131mpbird 256 . . . . . 6 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ Lim ๐ด)
133123, 132jca 512 . . . . 5 ((๐‘ฅ โˆˆ (On โˆ– 1o) โˆง ๐ด = (ฯ‰ ยทo ๐‘ฅ)) โ†’ (๐ด โˆˆ On โˆง Lim ๐ด))
134133rexlimiva 3147 . . . 4 (โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ) โ†’ (๐ด โˆˆ On โˆง Lim ๐ด))
135118, 134impbii 208 . . 3 ((๐ด โˆˆ On โˆง Lim ๐ด) โ†” โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ))
136135orbi2i 911 . 2 ((๐ด = On โˆจ (๐ด โˆˆ On โˆง Lim ๐ด)) โ†” (๐ด = On โˆจ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
1378, 13, 1363bitr2i 298 1 (Lim ๐ด โ†” (๐ด = On โˆจ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)๐ด = (ฯ‰ ยทo ๐‘ฅ)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆจ w3o 1086   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940  โˆƒwrex 3070  Vcvv 3474   โˆ– cdif 3944  โˆ…c0 4321  โˆช cuni 4907  Ord word 6360  Oncon0 6361  Lim wlim 6362  suc csuc 6363  (class class class)co 7405  ฯ‰com 7851  1oc1o 8455   +o coa 8459   ยทo comu 8460
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 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721  ax-inf2 9632
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-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  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-int 4950  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 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-oadd 8466  df-omul 8467
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator