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

Theorem oaabs2 8645
Description: The absorption law oaabs 8644 is also a property of higher powers of ฯ‰. (Contributed by Mario Carneiro, 29-May-2015.)
Assertion
Ref Expression
oaabs2 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (๐ด +o ๐ต) = ๐ต)

Proof of Theorem oaabs2
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 4333 . . . . . . 7 (๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†’ ยฌ (ฯ‰ โ†‘o ๐ถ) = โˆ…)
2 fnoe 8507 . . . . . . . . 9 โ†‘o Fn (On ร— On)
3 fndm 6650 . . . . . . . . 9 ( โ†‘o Fn (On ร— On) โ†’ dom โ†‘o = (On ร— On))
42, 3ax-mp 5 . . . . . . . 8 dom โ†‘o = (On ร— On)
54ndmov 7588 . . . . . . 7 (ยฌ (ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) = โˆ…)
61, 5nsyl2 141 . . . . . 6 (๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†’ (ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On))
76ad2antrr 725 . . . . 5 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On))
8 oecl 8534 . . . . 5 ((ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
97, 8syl 17 . . . 4 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
10 simplr 768 . . . 4 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ ๐ต โˆˆ On)
11 simpr 486 . . . 4 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต)
12 oawordeu 8552 . . . 4 ((((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ โˆƒ!๐‘ฅ โˆˆ On ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต)
139, 10, 11, 12syl21anc 837 . . 3 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ โˆƒ!๐‘ฅ โˆˆ On ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต)
14 reurex 3381 . . 3 (โˆƒ!๐‘ฅ โˆˆ On ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต โ†’ โˆƒ๐‘ฅ โˆˆ On ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต)
1513, 14syl 17 . 2 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ โˆƒ๐‘ฅ โˆˆ On ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต)
16 simpll 766 . . . . . . . 8 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ))
17 onelon 6387 . . . . . . . 8 (((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ ๐ด โˆˆ On)
189, 16, 17syl2anc 585 . . . . . . 7 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ ๐ด โˆˆ On)
1918adantr 482 . . . . . 6 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐ด โˆˆ On)
209adantr 482 . . . . . 6 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
21 simpr 486 . . . . . 6 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ On)
22 oaass 8558 . . . . . 6 ((๐ด โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด +o (ฯ‰ โ†‘o ๐ถ)) +o ๐‘ฅ) = (๐ด +o ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ)))
2319, 20, 21, 22syl3anc 1372 . . . . 5 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด +o (ฯ‰ โ†‘o ๐ถ)) +o ๐‘ฅ) = (๐ด +o ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ)))
247simprd 497 . . . . . . . . . 10 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ ๐ถ โˆˆ On)
25 eloni 6372 . . . . . . . . . 10 (๐ถ โˆˆ On โ†’ Ord ๐ถ)
2624, 25syl 17 . . . . . . . . 9 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ Ord ๐ถ)
27 ordzsl 7831 . . . . . . . . 9 (Ord ๐ถ โ†” (๐ถ = โˆ… โˆจ โˆƒ๐‘ฅ โˆˆ On ๐ถ = suc ๐‘ฅ โˆจ Lim ๐ถ))
2826, 27sylib 217 . . . . . . . 8 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (๐ถ = โˆ… โˆจ โˆƒ๐‘ฅ โˆˆ On ๐ถ = suc ๐‘ฅ โˆจ Lim ๐ถ))
29 simplll 774 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ))
30 oveq2 7414 . . . . . . . . . . . . . . 15 (๐ถ = โˆ… โ†’ (ฯ‰ โ†‘o ๐ถ) = (ฯ‰ โ†‘o โˆ…))
317simpld 496 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ ฯ‰ โˆˆ On)
32 oe0 8519 . . . . . . . . . . . . . . . 16 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o โˆ…) = 1o)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (ฯ‰ โ†‘o โˆ…) = 1o)
3430, 33sylan9eqr 2795 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ (ฯ‰ โ†‘o ๐ถ) = 1o)
3529, 34eleqtrd 2836 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ ๐ด โˆˆ 1o)
36 el1o 8492 . . . . . . . . . . . . 13 (๐ด โˆˆ 1o โ†” ๐ด = โˆ…)
3735, 36sylib 217 . . . . . . . . . . . 12 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ ๐ด = โˆ…)
3837oveq1d 7421 . . . . . . . . . . 11 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (โˆ… +o (ฯ‰ โ†‘o ๐ถ)))
399adantr 482 . . . . . . . . . . . 12 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
40 oa0r 8535 . . . . . . . . . . . 12 ((ฯ‰ โ†‘o ๐ถ) โˆˆ On โ†’ (โˆ… +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
4139, 40syl 17 . . . . . . . . . . 11 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ (โˆ… +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
4238, 41eqtrd 2773 . . . . . . . . . 10 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐ถ = โˆ…) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
4342ex 414 . . . . . . . . 9 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (๐ถ = โˆ… โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ)))
4431adantr 482 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ ฯ‰ โˆˆ On)
45 simprl 770 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ On)
46 oecl 8534 . . . . . . . . . . . . . 14 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
4744, 45, 46syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
48 limom 7868 . . . . . . . . . . . . . 14 Lim ฯ‰
4944, 48jctir 522 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (ฯ‰ โˆˆ On โˆง Lim ฯ‰))
50 simplll 774 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ))
51 simprr 772 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ ๐ถ = suc ๐‘ฅ)
5251oveq2d 7422 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐ถ) = (ฯ‰ โ†‘o suc ๐‘ฅ))
53 oesuc 8524 . . . . . . . . . . . . . . . 16 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o suc ๐‘ฅ) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰))
5444, 45, 53syl2anc 585 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o suc ๐‘ฅ) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰))
5552, 54eqtrd 2773 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐ถ) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰))
5650, 55eleqtrd 2836 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰))
57 omordlim 8574 . . . . . . . . . . . . 13 ((((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง (ฯ‰ โˆˆ On โˆง Lim ฯ‰)) โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰)) โ†’ โˆƒ๐‘ฆ โˆˆ ฯ‰ ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
5847, 49, 56, 57syl21anc 837 . . . . . . . . . . . 12 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ โˆƒ๐‘ฆ โˆˆ ฯ‰ ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
5947adantr 482 . . . . . . . . . . . . . . . . 17 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
60 nnon 7858 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ ฯ‰ โ†’ ๐‘ฆ โˆˆ On)
6160ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ๐‘ฆ โˆˆ On)
62 omcl 8533 . . . . . . . . . . . . . . . . 17 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On)
6359, 61, 62syl2anc 585 . . . . . . . . . . . . . . . 16 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On)
64 eloni 6372 . . . . . . . . . . . . . . . 16 (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On โ†’ Ord ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
6563, 64syl 17 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ Ord ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
66 simprr 772 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
67 ordelss 6378 . . . . . . . . . . . . . . 15 ((Ord ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ)) โ†’ ๐ด โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
6865, 66, 67syl2anc 585 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ๐ด โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
6918ad2antrr 725 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ๐ด โˆˆ On)
709ad2antrr 725 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
71 oawordri 8547 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (๐ด โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐ถ))))
7269, 63, 70, 71syl3anc 1372 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (๐ด โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐ถ))))
7368, 72mpd 15 . . . . . . . . . . . . 13 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐ถ)))
7444adantr 482 . . . . . . . . . . . . . . . 16 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ฯ‰ โˆˆ On)
75 odi 8576 . . . . . . . . . . . . . . . 16 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On โˆง ฯ‰ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (๐‘ฆ +o ฯ‰)) = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰)))
7659, 61, 74, 75syl3anc 1372 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (๐‘ฆ +o ฯ‰)) = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰)))
77 simprl 770 . . . . . . . . . . . . . . . . 17 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ๐‘ฆ โˆˆ ฯ‰)
78 oaabslem 8643 . . . . . . . . . . . . . . . . 17 ((ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o ฯ‰) = ฯ‰)
7974, 77, 78syl2anc 585 . . . . . . . . . . . . . . . 16 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (๐‘ฆ +o ฯ‰) = ฯ‰)
8079oveq2d 7422 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (๐‘ฆ +o ฯ‰)) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰))
8176, 80eqtr3d 2775 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰)) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰))
8255adantr 482 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐ถ) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰))
8382oveq2d 7422 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐ถ)) = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ฯ‰)))
8481, 83, 823eqtr4d 2783 . . . . . . . . . . . . 13 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
8573, 84sseqtrd 4022 . . . . . . . . . . . 12 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โˆง (๐‘ฆ โˆˆ ฯ‰ โˆง ๐ด โˆˆ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (ฯ‰ โ†‘o ๐ถ))
8658, 85rexlimddv 3162 . . . . . . . . . . 11 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (ฯ‰ โ†‘o ๐ถ))
87 oaword2 8550 . . . . . . . . . . . . 13 (((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) โŠ† (๐ด +o (ฯ‰ โ†‘o ๐ถ)))
889, 18, 87syl2anc 585 . . . . . . . . . . . 12 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (ฯ‰ โ†‘o ๐ถ) โŠ† (๐ด +o (ฯ‰ โ†‘o ๐ถ)))
8988adantr 482 . . . . . . . . . . 11 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐ถ) โŠ† (๐ด +o (ฯ‰ โ†‘o ๐ถ)))
9086, 89eqssd 3999 . . . . . . . . . 10 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง (๐‘ฅ โˆˆ On โˆง ๐ถ = suc ๐‘ฅ)) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
9190rexlimdvaa 3157 . . . . . . . . 9 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (โˆƒ๐‘ฅ โˆˆ On ๐ถ = suc ๐‘ฅ โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ)))
92 simplll 774 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ))
9331adantr 482 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ ฯ‰ โˆˆ On)
9424adantr 482 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ ๐ถ โˆˆ On)
95 simpr 486 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ Lim ๐ถ)
96 oelim2 8592 . . . . . . . . . . . . . . 15 ((ฯ‰ โˆˆ On โˆง (๐ถ โˆˆ On โˆง Lim ๐ถ)) โ†’ (ฯ‰ โ†‘o ๐ถ) = โˆช ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฅ))
9793, 94, 95, 96syl12anc 836 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (ฯ‰ โ†‘o ๐ถ) = โˆช ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฅ))
9892, 97eleqtrd 2836 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ ๐ด โˆˆ โˆช ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฅ))
99 eliun 5001 . . . . . . . . . . . . 13 (๐ด โˆˆ โˆช ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฅ) โ†” โˆƒ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
10098, 99sylib 217 . . . . . . . . . . . 12 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ โˆƒ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
101 eldifi 4126 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ (๐ถ โˆ– 1o) โ†’ ๐‘ฅ โˆˆ ๐ถ)
10218ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ ๐ด โˆˆ On)
1039ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
10493adantr 482 . . . . . . . . . . . . . . . . . . 19 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ ฯ‰ โˆˆ On)
105 1onn 8636 . . . . . . . . . . . . . . . . . . 19 1o โˆˆ ฯ‰
106 ondif2 8499 . . . . . . . . . . . . . . . . . . 19 (ฯ‰ โˆˆ (On โˆ– 2o) โ†” (ฯ‰ โˆˆ On โˆง 1o โˆˆ ฯ‰))
107104, 105, 106sylanblrc 591 . . . . . . . . . . . . . . . . . 18 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
10894adantr 482 . . . . . . . . . . . . . . . . . 18 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ ๐ถ โˆˆ On)
109 simplr 768 . . . . . . . . . . . . . . . . . 18 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ Lim ๐ถ)
110 oelimcl 8597 . . . . . . . . . . . . . . . . . 18 ((ฯ‰ โˆˆ (On โˆ– 2o) โˆง (๐ถ โˆˆ On โˆง Lim ๐ถ)) โ†’ Lim (ฯ‰ โ†‘o ๐ถ))
111107, 108, 109, 110syl12anc 836 . . . . . . . . . . . . . . . . 17 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ Lim (ฯ‰ โ†‘o ๐ถ))
112 oalim 8529 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ On โˆง ((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง Lim (ฯ‰ โ†‘o ๐ถ))) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = โˆช ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ)(๐ด +o ๐‘ฆ))
113102, 103, 111, 112syl12anc 836 . . . . . . . . . . . . . . . 16 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = โˆช ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ)(๐ด +o ๐‘ฆ))
114 oelim2 8592 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โˆˆ On โˆง (๐ถ โˆˆ On โˆง Lim ๐ถ)) โ†’ (ฯ‰ โ†‘o ๐ถ) = โˆช ๐‘ง โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ง))
11593, 94, 95, 114syl12anc 836 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (ฯ‰ โ†‘o ๐ถ) = โˆช ๐‘ง โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ง))
116115eleq2d 2820 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” ๐‘ฆ โˆˆ โˆช ๐‘ง โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ง)))
117 eliun 5001 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ โˆช ๐‘ง โˆˆ (๐ถ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ง) โ†” โˆƒ๐‘ง โˆˆ (๐ถ โˆ– 1o)๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))
118116, 117bitrdi 287 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” โˆƒ๐‘ง โˆˆ (๐ถ โˆ– 1o)๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง)))
119118adantr 482 . . . . . . . . . . . . . . . . . . 19 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ (๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” โˆƒ๐‘ง โˆˆ (๐ถ โˆ– 1o)๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง)))
120 eldifi 4126 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ง โˆˆ (๐ถ โˆ– 1o) โ†’ ๐‘ง โˆˆ ๐ถ)
121104adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ฯ‰ โˆˆ On)
122108adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐ถ โˆˆ On)
123 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ฅ โˆˆ ๐ถ)
124 onelon 6387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ ๐‘ฅ โˆˆ On)
125122, 123, 124syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ฅ โˆˆ On)
126121, 125, 46syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
127 eloni 6372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โ†’ Ord (ฯ‰ โ†‘o ๐‘ฅ))
128126, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ Ord (ฯ‰ โ†‘o ๐‘ฅ))
129 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
130 ordelss 6378 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐ด โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
131128, 129, 130syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐ด โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
132 ssun1 4172 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ๐‘ฅ โŠ† (๐‘ฅ โˆช ๐‘ง)
13326ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ Ord ๐ถ)
134 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ง โˆˆ ๐ถ)
135 ordunel 7812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Ord ๐ถ โˆง ๐‘ฅ โˆˆ ๐ถ โˆง ๐‘ง โˆˆ ๐ถ) โ†’ (๐‘ฅ โˆช ๐‘ง) โˆˆ ๐ถ)
136133, 123, 134, 135syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐‘ฅ โˆช ๐‘ง) โˆˆ ๐ถ)
137 onelon 6387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐ถ โˆˆ On โˆง (๐‘ฅ โˆช ๐‘ง) โˆˆ ๐ถ) โ†’ (๐‘ฅ โˆช ๐‘ง) โˆˆ On)
138122, 136, 137syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐‘ฅ โˆช ๐‘ง) โˆˆ On)
139 peano1 7876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 โˆ… โˆˆ ฯ‰
140139a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ โˆ… โˆˆ ฯ‰)
141 oewordi 8588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐‘ฅ โˆˆ On โˆง (๐‘ฅ โˆช ๐‘ง) โˆˆ On โˆง ฯ‰ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ (๐‘ฅ โŠ† (๐‘ฅ โˆช ๐‘ง) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
142125, 138, 121, 140, 141syl31anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐‘ฅ โŠ† (๐‘ฅ โˆช ๐‘ง) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
143132, 142mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))
144131, 143sstrd 3992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))
145102adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐ด โˆˆ On)
146 oecl 8534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ฯ‰ โˆˆ On โˆง (๐‘ฅ โˆช ๐‘ง) โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On)
147121, 138, 146syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On)
148 onelon 6387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐ถ โˆˆ On โˆง ๐‘ง โˆˆ ๐ถ) โ†’ ๐‘ง โˆˆ On)
149122, 134, 148syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ง โˆˆ On)
150 oecl 8534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ฯ‰ โˆˆ On โˆง ๐‘ง โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ง) โˆˆ On)
151121, 149, 150syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (ฯ‰ โ†‘o ๐‘ง) โˆˆ On)
152 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))
153 onelon 6387 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ฯ‰ โ†‘o ๐‘ง) โˆˆ On โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง)) โ†’ ๐‘ฆ โˆˆ On)
154151, 152, 153syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ฆ โˆˆ On)
155 oawordri 8547 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐ด โˆˆ On โˆง (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โ†’ (๐ด +o ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o ๐‘ฆ)))
156145, 147, 154, 155syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โ†’ (๐ด +o ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o ๐‘ฆ)))
157144, 156mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐ด +o ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o ๐‘ฆ))
158 eloni 6372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ฯ‰ โ†‘o ๐‘ง) โˆˆ On โ†’ Ord (ฯ‰ โ†‘o ๐‘ง))
159151, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ Ord (ฯ‰ โ†‘o ๐‘ง))
160 ordelss 6378 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ฯ‰ โ†‘o ๐‘ง) โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง)) โ†’ ๐‘ฆ โŠ† (ฯ‰ โ†‘o ๐‘ง))
161159, 152, 160syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ฆ โŠ† (ฯ‰ โ†‘o ๐‘ง))
162 ssun2 4173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ๐‘ง โŠ† (๐‘ฅ โˆช ๐‘ง)
163 oewordi 8588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐‘ง โˆˆ On โˆง (๐‘ฅ โˆช ๐‘ง) โˆˆ On โˆง ฯ‰ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ (๐‘ง โŠ† (๐‘ฅ โˆช ๐‘ง) โ†’ (ฯ‰ โ†‘o ๐‘ง) โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
164149, 138, 121, 140, 163syl31anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐‘ง โŠ† (๐‘ฅ โˆช ๐‘ง) โ†’ (ฯ‰ โ†‘o ๐‘ง) โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
165162, 164mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (ฯ‰ โ†‘o ๐‘ง) โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))
166161, 165sstrd 3992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ๐‘ฆ โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))
167 oaword 8546 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ On โˆง (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On โˆง (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On) โ†’ (๐‘ฆ โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โ†” ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))))
168154, 147, 147, 167syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐‘ฆ โŠ† (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โ†” ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))))
169166, 168mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
170157, 169sstrd 3992 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐ด +o ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
171 ordom 7862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ord ฯ‰
172 ordsucss 7803 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Ord ฯ‰ โ†’ (1o โˆˆ ฯ‰ โ†’ suc 1o โŠ† ฯ‰))
173171, 105, 172mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26 suc 1o โŠ† ฯ‰
174 1on 8475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1o โˆˆ On
175 onsuc 7796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1o โˆˆ On โ†’ suc 1o โˆˆ On)
176174, 175mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ suc 1o โˆˆ On)
177 omwordi 8568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 1o โˆˆ On โˆง ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On) โ†’ (suc 1o โŠ† ฯ‰ โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo suc 1o) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo ฯ‰)))
178176, 121, 147, 177syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (suc 1o โŠ† ฯ‰ โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo suc 1o) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo ฯ‰)))
179173, 178mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo suc 1o) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo ฯ‰))
180174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ 1o โˆˆ On)
181 omsuc 8523 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On โˆง 1o โˆˆ On) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo suc 1o) = (((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo 1o) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
182147, 180, 181syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo suc 1o) = (((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo 1o) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
183 om1 8539 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) โˆˆ On โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo 1o) = (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))
184147, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo 1o) = (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)))
185184oveq1d 7421 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo 1o) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))) = ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))))
186182, 185eqtr2d 2774 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))) = ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo suc 1o))
187 oesuc 8524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ฯ‰ โˆˆ On โˆง (๐‘ฅ โˆช ๐‘ง) โˆˆ On) โ†’ (ฯ‰ โ†‘o suc (๐‘ฅ โˆช ๐‘ง)) = ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo ฯ‰))
188121, 138, 187syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (ฯ‰ โ†‘o suc (๐‘ฅ โˆช ๐‘ง)) = ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) ยทo ฯ‰))
189179, 186, 1883sstr4d 4029 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง)) +o (ฯ‰ โ†‘o (๐‘ฅ โˆช ๐‘ง))) โŠ† (ฯ‰ โ†‘o suc (๐‘ฅ โˆช ๐‘ง)))
190170, 189sstrd 3992 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o suc (๐‘ฅ โˆช ๐‘ง)))
191 ordsucss 7803 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord ๐ถ โ†’ ((๐‘ฅ โˆช ๐‘ง) โˆˆ ๐ถ โ†’ suc (๐‘ฅ โˆช ๐‘ง) โŠ† ๐ถ))
192133, 136, 191sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ suc (๐‘ฅ โˆช ๐‘ง) โŠ† ๐ถ)
193 onsuc 7796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฅ โˆช ๐‘ง) โˆˆ On โ†’ suc (๐‘ฅ โˆช ๐‘ง) โˆˆ On)
194138, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ suc (๐‘ฅ โˆช ๐‘ง) โˆˆ On)
195 oewordi 8588 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((suc (๐‘ฅ โˆช ๐‘ง) โˆˆ On โˆง ๐ถ โˆˆ On โˆง ฯ‰ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ (suc (๐‘ฅ โˆช ๐‘ง) โŠ† ๐ถ โ†’ (ฯ‰ โ†‘o suc (๐‘ฅ โˆช ๐‘ง)) โŠ† (ฯ‰ โ†‘o ๐ถ)))
196194, 122, 121, 140, 195syl31anc 1374 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (suc (๐‘ฅ โˆช ๐‘ง) โŠ† ๐ถ โ†’ (ฯ‰ โ†‘o suc (๐‘ฅ โˆช ๐‘ง)) โŠ† (ฯ‰ โ†‘o ๐ถ)))
197192, 196mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (ฯ‰ โ†‘o suc (๐‘ฅ โˆช ๐‘ง)) โŠ† (ฯ‰ โ†‘o ๐ถ))
198190, 197sstrd 3992 . . . . . . . . . . . . . . . . . . . . . 22 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง (๐‘ง โˆˆ ๐ถ โˆง ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง))) โ†’ (๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ))
199198expr 458 . . . . . . . . . . . . . . . . . . . . 21 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง ๐‘ง โˆˆ ๐ถ) โ†’ (๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง) โ†’ (๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ)))
200120, 199sylan2 594 . . . . . . . . . . . . . . . . . . . 20 ((((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โˆง ๐‘ง โˆˆ (๐ถ โˆ– 1o)) โ†’ (๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง) โ†’ (๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ)))
201200rexlimdva 3156 . . . . . . . . . . . . . . . . . . 19 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ (โˆƒ๐‘ง โˆˆ (๐ถ โˆ– 1o)๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐‘ง) โ†’ (๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ)))
202119, 201sylbid 239 . . . . . . . . . . . . . . . . . 18 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ (๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†’ (๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ)))
203202ralrimiv 3146 . . . . . . . . . . . . . . . . 17 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ โˆ€๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ)(๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ))
204 iunss 5048 . . . . . . . . . . . . . . . . 17 (โˆช ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ)(๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ) โ†” โˆ€๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ)(๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ))
205203, 204sylibr 233 . . . . . . . . . . . . . . . 16 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ โˆช ๐‘ฆ โˆˆ (ฯ‰ โ†‘o ๐ถ)(๐ด +o ๐‘ฆ) โŠ† (ฯ‰ โ†‘o ๐ถ))
206113, 205eqsstrd 4020 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง (๐‘ฅ โˆˆ ๐ถ โˆง ๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (ฯ‰ โ†‘o ๐ถ))
207206expr 458 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ (๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (ฯ‰ โ†‘o ๐ถ)))
208101, 207sylan2 594 . . . . . . . . . . . . 13 (((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โˆง ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)) โ†’ (๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (ฯ‰ โ†‘o ๐ถ)))
209208rexlimdva 3156 . . . . . . . . . . . 12 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (โˆƒ๐‘ฅ โˆˆ (๐ถ โˆ– 1o)๐ด โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (ฯ‰ โ†‘o ๐ถ)))
210100, 209mpd 15 . . . . . . . . . . 11 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) โŠ† (ฯ‰ โ†‘o ๐ถ))
21188adantr 482 . . . . . . . . . . 11 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (ฯ‰ โ†‘o ๐ถ) โŠ† (๐ด +o (ฯ‰ โ†‘o ๐ถ)))
212210, 211eqssd 3999 . . . . . . . . . 10 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง Lim ๐ถ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
213212ex 414 . . . . . . . . 9 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (Lim ๐ถ โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ)))
21443, 91, 2133jaod 1429 . . . . . . . 8 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ ((๐ถ = โˆ… โˆจ โˆƒ๐‘ฅ โˆˆ On ๐ถ = suc ๐‘ฅ โˆจ Lim ๐ถ) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ)))
21528, 214mpd 15 . . . . . . 7 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
216215adantr 482 . . . . . 6 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
217216oveq1d 7421 . . . . 5 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด +o (ฯ‰ โ†‘o ๐ถ)) +o ๐‘ฅ) = ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ))
21823, 217eqtr3d 2775 . . . 4 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด +o ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ)) = ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ))
219 oveq2 7414 . . . . 5 (((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต โ†’ (๐ด +o ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ)) = (๐ด +o ๐ต))
220 id 22 . . . . 5 (((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต โ†’ ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต)
221219, 220eqeq12d 2749 . . . 4 (((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต โ†’ ((๐ด +o ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ)) = ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) โ†” (๐ด +o ๐ต) = ๐ต))
222218, 221syl5ibcom 244 . . 3 ((((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โˆง ๐‘ฅ โˆˆ On) โ†’ (((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต โ†’ (๐ด +o ๐ต) = ๐ต))
223222rexlimdva 3156 . 2 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (โˆƒ๐‘ฅ โˆˆ On ((ฯ‰ โ†‘o ๐ถ) +o ๐‘ฅ) = ๐ต โ†’ (๐ด +o ๐ต) = ๐ต))
22415, 223mpd 15 1 (((๐ด โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง ๐ต โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† ๐ต) โ†’ (๐ด +o ๐ต) = ๐ต)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ w3o 1087   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3062  โˆƒwrex 3071  โˆƒ!wreu 3375   โˆ– cdif 3945   โˆช cun 3946   โŠ† wss 3948  โˆ…c0 4322  โˆช ciun 4997   ร— cxp 5674  dom cdm 5676  Ord word 6361  Oncon0 6362  Lim wlim 6363  suc csuc 6364   Fn wfn 6536  (class class class)co 7406  ฯ‰com 7852  1oc1o 8456  2oc2o 8457   +o coa 8460   ยทo comu 8461   โ†‘o coe 8462
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 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-oadd 8467  df-omul 8468  df-oexp 8469
This theorem is referenced by:  cnfcomlem  9691  oacl2g  42066  omabs2  42068  ofoaf  42091
  Copyright terms: Public domain W3C validator