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

Theorem naddwordnexlem4 42754
Description: When ๐ด is the sum of a limit ordinal (or zero) and a natural number and ๐ต is the sum of a larger limit ordinal and a smaller natural number, there exists a product with omega such that the ordinal sum with ๐ด is less than or equal to ๐ต while the natural sum is larger than ๐ต. (Contributed by RP, 15-Feb-2025.)
Hypotheses
Ref Expression
naddwordnex.a (๐œ‘ โ†’ ๐ด = ((ฯ‰ ยทo ๐ถ) +o ๐‘€))
naddwordnex.b (๐œ‘ โ†’ ๐ต = ((ฯ‰ ยทo ๐ท) +o ๐‘))
naddwordnex.c (๐œ‘ โ†’ ๐ถ โˆˆ ๐ท)
naddwordnex.d (๐œ‘ โ†’ ๐ท โˆˆ On)
naddwordnex.m (๐œ‘ โ†’ ๐‘€ โˆˆ ฯ‰)
naddwordnex.n (๐œ‘ โ†’ ๐‘ โˆˆ ๐‘€)
naddwordnexlem4.s ๐‘† = {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}
Assertion
Ref Expression
naddwordnexlem4 (๐œ‘ โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)((๐ถ +o ๐‘ฅ) = ๐ท โˆง (๐ด +o (ฯ‰ ยทo ๐‘ฅ)) โІ ๐ต โˆง ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo ๐‘ฅ))))
Distinct variable groups:   ๐‘ฅ,๐ด   ๐‘ฅ,๐ต   ๐‘ฅ,๐ถ,๐‘ฆ   ๐‘ฅ,๐ท,๐‘ฆ   ๐‘ฅ,๐‘†   ๐œ‘,๐‘ฆ
Allowed substitution hints:   ๐œ‘(๐‘ฅ)   ๐ด(๐‘ฆ)   ๐ต(๐‘ฆ)   ๐‘†(๐‘ฆ)   ๐‘€(๐‘ฅ,๐‘ฆ)   ๐‘(๐‘ฅ,๐‘ฆ)

Proof of Theorem naddwordnexlem4
Dummy variable ๐‘ง is distinct from all other variables.
StepHypRef Expression
1 naddwordnexlem4.s . . . . 5 ๐‘† = {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}
21ssrab3 4076 . . . 4 ๐‘† โІ On
3 oveq2 7422 . . . . . . . 8 (๐‘ฆ = ๐ท โ†’ (๐ถ +o ๐‘ฆ) = (๐ถ +o ๐ท))
43sseq2d 4010 . . . . . . 7 (๐‘ฆ = ๐ท โ†’ (๐ท โІ (๐ถ +o ๐‘ฆ) โ†” ๐ท โІ (๐ถ +o ๐ท)))
5 naddwordnex.d . . . . . . 7 (๐œ‘ โ†’ ๐ท โˆˆ On)
6 naddwordnex.c . . . . . . . . 9 (๐œ‘ โ†’ ๐ถ โˆˆ ๐ท)
7 onelon 6388 . . . . . . . . 9 ((๐ท โˆˆ On โˆง ๐ถ โˆˆ ๐ท) โ†’ ๐ถ โˆˆ On)
85, 6, 7syl2anc 583 . . . . . . . 8 (๐œ‘ โ†’ ๐ถ โˆˆ On)
9 oaword2 8567 . . . . . . . 8 ((๐ท โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ๐ท โІ (๐ถ +o ๐ท))
105, 8, 9syl2anc 583 . . . . . . 7 (๐œ‘ โ†’ ๐ท โІ (๐ถ +o ๐ท))
114, 5, 10elrabd 3682 . . . . . 6 (๐œ‘ โ†’ ๐ท โˆˆ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)})
1211, 1eleqtrrdi 2839 . . . . 5 (๐œ‘ โ†’ ๐ท โˆˆ ๐‘†)
1312ne0d 4331 . . . 4 (๐œ‘ โ†’ ๐‘† โ‰  โˆ…)
14 oninton 7792 . . . 4 ((๐‘† โІ On โˆง ๐‘† โ‰  โˆ…) โ†’ โˆฉ ๐‘† โˆˆ On)
152, 13, 14sylancr 586 . . 3 (๐œ‘ โ†’ โˆฉ ๐‘† โˆˆ On)
16 oveq2 7422 . . . . . . . . . . . . 13 (๐‘ฆ = โˆ… โ†’ (๐ถ +o ๐‘ฆ) = (๐ถ +o โˆ…))
17 oa0 8530 . . . . . . . . . . . . . 14 (๐ถ โˆˆ On โ†’ (๐ถ +o โˆ…) = ๐ถ)
188, 17syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ถ +o โˆ…) = ๐ถ)
1916, 18sylan9eqr 2789 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฆ = โˆ…) โ†’ (๐ถ +o ๐‘ฆ) = ๐ถ)
206adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฆ = โˆ…) โ†’ ๐ถ โˆˆ ๐ท)
2119, 20eqeltrd 2828 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฆ = โˆ…) โ†’ (๐ถ +o ๐‘ฆ) โˆˆ ๐ท)
2221ex 412 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฆ = โˆ… โ†’ (๐ถ +o ๐‘ฆ) โˆˆ ๐ท))
2322adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฆ โˆˆ On) โ†’ (๐‘ฆ = โˆ… โ†’ (๐ถ +o ๐‘ฆ) โˆˆ ๐ท))
2423con3d 152 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฆ โˆˆ On) โ†’ (ยฌ (๐ถ +o ๐‘ฆ) โˆˆ ๐ท โ†’ ยฌ ๐‘ฆ = โˆ…))
25 oacl 8549 . . . . . . . . . 10 ((๐ถ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ +o ๐‘ฆ) โˆˆ On)
268, 25sylan 579 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ +o ๐‘ฆ) โˆˆ On)
27 ontri1 6397 . . . . . . . . 9 ((๐ท โˆˆ On โˆง (๐ถ +o ๐‘ฆ) โˆˆ On) โ†’ (๐ท โІ (๐ถ +o ๐‘ฆ) โ†” ยฌ (๐ถ +o ๐‘ฆ) โˆˆ ๐ท))
285, 26, 27syl2an2r 684 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ท โІ (๐ถ +o ๐‘ฆ) โ†” ยฌ (๐ถ +o ๐‘ฆ) โˆˆ ๐ท))
29 on0eln0 6419 . . . . . . . . . 10 (๐‘ฆ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฆ โ†” ๐‘ฆ โ‰  โˆ…))
30 df-ne 2936 . . . . . . . . . 10 (๐‘ฆ โ‰  โˆ… โ†” ยฌ ๐‘ฆ = โˆ…)
3129, 30bitrdi 287 . . . . . . . . 9 (๐‘ฆ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฆ โ†” ยฌ ๐‘ฆ = โˆ…))
3231adantl 481 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฆ โˆˆ On) โ†’ (โˆ… โˆˆ ๐‘ฆ โ†” ยฌ ๐‘ฆ = โˆ…))
3324, 28, 323imtr4d 294 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ท โІ (๐ถ +o ๐‘ฆ) โ†’ โˆ… โˆˆ ๐‘ฆ))
3433ex 412 . . . . . 6 (๐œ‘ โ†’ (๐‘ฆ โˆˆ On โ†’ (๐ท โІ (๐ถ +o ๐‘ฆ) โ†’ โˆ… โˆˆ ๐‘ฆ)))
3534ralrimiv 3140 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ On (๐ท โІ (๐ถ +o ๐‘ฆ) โ†’ โˆ… โˆˆ ๐‘ฆ))
36 0ex 5301 . . . . . 6 โˆ… โˆˆ V
3736elintrab 4958 . . . . 5 (โˆ… โˆˆ โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)} โ†” โˆ€๐‘ฆ โˆˆ On (๐ท โІ (๐ถ +o ๐‘ฆ) โ†’ โˆ… โˆˆ ๐‘ฆ))
3835, 37sylibr 233 . . . 4 (๐œ‘ โ†’ โˆ… โˆˆ โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)})
391inteqi 4948 . . . 4 โˆฉ ๐‘† = โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}
4038, 39eleqtrrdi 2839 . . 3 (๐œ‘ โ†’ โˆ… โˆˆ โˆฉ ๐‘†)
41 ondif1 8515 . . 3 (โˆฉ ๐‘† โˆˆ (On โˆ– 1o) โ†” (โˆฉ ๐‘† โˆˆ On โˆง โˆ… โˆˆ โˆฉ ๐‘†))
4215, 40, 41sylanbrc 582 . 2 (๐œ‘ โ†’ โˆฉ ๐‘† โˆˆ (On โˆ– 1o))
43 onzsl 7844 . . . . . 6 (โˆฉ ๐‘† โˆˆ On โ†” (โˆฉ ๐‘† = โˆ… โˆจ โˆƒ๐‘ง โˆˆ On โˆฉ ๐‘† = suc ๐‘ง โˆจ (โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†)))
4415, 43sylib 217 . . . . 5 (๐œ‘ โ†’ (โˆฉ ๐‘† = โˆ… โˆจ โˆƒ๐‘ง โˆˆ On โˆฉ ๐‘† = suc ๐‘ง โˆจ (โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†)))
45 oveq2 7422 . . . . . . . . 9 (โˆฉ ๐‘† = โˆ… โ†’ (๐ถ +o โˆฉ ๐‘†) = (๐ถ +o โˆ…))
4645, 18sylan9eqr 2789 . . . . . . . 8 ((๐œ‘ โˆง โˆฉ ๐‘† = โˆ…) โ†’ (๐ถ +o โˆฉ ๐‘†) = ๐ถ)
47 onelpss 6403 . . . . . . . . . . . 12 ((๐ถ โˆˆ On โˆง ๐ท โˆˆ On) โ†’ (๐ถ โˆˆ ๐ท โ†” (๐ถ โІ ๐ท โˆง ๐ถ โ‰  ๐ท)))
488, 5, 47syl2anc 583 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ถ โˆˆ ๐ท โ†” (๐ถ โІ ๐ท โˆง ๐ถ โ‰  ๐ท)))
496, 48mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ถ โІ ๐ท โˆง ๐ถ โ‰  ๐ท))
5049simpld 494 . . . . . . . . 9 (๐œ‘ โ†’ ๐ถ โІ ๐ท)
5150adantr 480 . . . . . . . 8 ((๐œ‘ โˆง โˆฉ ๐‘† = โˆ…) โ†’ ๐ถ โІ ๐ท)
5246, 51eqsstrd 4016 . . . . . . 7 ((๐œ‘ โˆง โˆฉ ๐‘† = โˆ…) โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท)
5352ex 412 . . . . . 6 (๐œ‘ โ†’ (โˆฉ ๐‘† = โˆ… โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท))
54 oveq2 7422 . . . . . . . . 9 (โˆฉ ๐‘† = suc ๐‘ง โ†’ (๐ถ +o โˆฉ ๐‘†) = (๐ถ +o suc ๐‘ง))
55 oasuc 8538 . . . . . . . . . 10 ((๐ถ โˆˆ On โˆง ๐‘ง โˆˆ On) โ†’ (๐ถ +o suc ๐‘ง) = suc (๐ถ +o ๐‘ง))
568, 55sylan 579 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (๐ถ +o suc ๐‘ง) = suc (๐ถ +o ๐‘ง))
5754, 56sylan9eqr 2789 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ง โˆˆ On) โˆง โˆฉ ๐‘† = suc ๐‘ง) โ†’ (๐ถ +o โˆฉ ๐‘†) = suc (๐ถ +o ๐‘ง))
58 vex 3473 . . . . . . . . . . . . 13 ๐‘ง โˆˆ V
5958sucid 6445 . . . . . . . . . . . 12 ๐‘ง โˆˆ suc ๐‘ง
60 eleq2 2817 . . . . . . . . . . . 12 (โˆฉ ๐‘† = suc ๐‘ง โ†’ (๐‘ง โˆˆ โˆฉ ๐‘† โ†” ๐‘ง โˆˆ suc ๐‘ง))
6159, 60mpbiri 258 . . . . . . . . . . 11 (โˆฉ ๐‘† = suc ๐‘ง โ†’ ๐‘ง โˆˆ โˆฉ ๐‘†)
6261a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (โˆฉ ๐‘† = suc ๐‘ง โ†’ ๐‘ง โˆˆ โˆฉ ๐‘†))
6339eleq2i 2820 . . . . . . . . . . . 12 (๐‘ง โˆˆ โˆฉ ๐‘† โ†” ๐‘ง โˆˆ โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)})
64 oveq2 7422 . . . . . . . . . . . . . . 15 (๐‘ฆ = ๐‘ง โ†’ (๐ถ +o ๐‘ฆ) = (๐ถ +o ๐‘ง))
6564sseq2d 4010 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ง โ†’ (๐ท โІ (๐ถ +o ๐‘ฆ) โ†” ๐ท โІ (๐ถ +o ๐‘ง)))
6665onnminsb 7796 . . . . . . . . . . . . 13 (๐‘ง โˆˆ On โ†’ (๐‘ง โˆˆ โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)} โ†’ ยฌ ๐ท โІ (๐ถ +o ๐‘ง)))
6766adantl 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (๐‘ง โˆˆ โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)} โ†’ ยฌ ๐ท โІ (๐ถ +o ๐‘ง)))
6863, 67biimtrid 241 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (๐‘ง โˆˆ โˆฉ ๐‘† โ†’ ยฌ ๐ท โІ (๐ถ +o ๐‘ง)))
69 oacl 8549 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ On โˆง ๐‘ง โˆˆ On) โ†’ (๐ถ +o ๐‘ง) โˆˆ On)
708, 69sylan 579 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (๐ถ +o ๐‘ง) โˆˆ On)
71 ontri1 6397 . . . . . . . . . . . . 13 ((๐ท โˆˆ On โˆง (๐ถ +o ๐‘ง) โˆˆ On) โ†’ (๐ท โІ (๐ถ +o ๐‘ง) โ†” ยฌ (๐ถ +o ๐‘ง) โˆˆ ๐ท))
725, 70, 71syl2an2r 684 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (๐ท โІ (๐ถ +o ๐‘ง) โ†” ยฌ (๐ถ +o ๐‘ง) โˆˆ ๐ท))
7372con2bid 354 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ ((๐ถ +o ๐‘ง) โˆˆ ๐ท โ†” ยฌ ๐ท โІ (๐ถ +o ๐‘ง)))
7468, 73sylibrd 259 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (๐‘ง โˆˆ โˆฉ ๐‘† โ†’ (๐ถ +o ๐‘ง) โˆˆ ๐ท))
75 onsucss 42618 . . . . . . . . . . . 12 (๐ท โˆˆ On โ†’ ((๐ถ +o ๐‘ง) โˆˆ ๐ท โ†’ suc (๐ถ +o ๐‘ง) โІ ๐ท))
765, 75syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ถ +o ๐‘ง) โˆˆ ๐ท โ†’ suc (๐ถ +o ๐‘ง) โІ ๐ท))
7776adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ ((๐ถ +o ๐‘ง) โˆˆ ๐ท โ†’ suc (๐ถ +o ๐‘ง) โІ ๐ท))
7862, 74, 773syld 60 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ On) โ†’ (โˆฉ ๐‘† = suc ๐‘ง โ†’ suc (๐ถ +o ๐‘ง) โІ ๐ท))
7978imp 406 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ง โˆˆ On) โˆง โˆฉ ๐‘† = suc ๐‘ง) โ†’ suc (๐ถ +o ๐‘ง) โІ ๐ท)
8057, 79eqsstrd 4016 . . . . . . 7 (((๐œ‘ โˆง ๐‘ง โˆˆ On) โˆง โˆฉ ๐‘† = suc ๐‘ง) โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท)
8180rexlimdva2 3152 . . . . . 6 (๐œ‘ โ†’ (โˆƒ๐‘ง โˆˆ On โˆฉ ๐‘† = suc ๐‘ง โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท))
82 oalim 8546 . . . . . . . . 9 ((๐ถ โˆˆ On โˆง (โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†)) โ†’ (๐ถ +o โˆฉ ๐‘†) = โˆช ๐‘ง โˆˆ โˆฉ ๐‘†(๐ถ +o ๐‘ง))
838, 82sylan 579 . . . . . . . 8 ((๐œ‘ โˆง (โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†)) โ†’ (๐ถ +o โˆฉ ๐‘†) = โˆช ๐‘ง โˆˆ โˆฉ ๐‘†(๐ถ +o ๐‘ง))
84 onelon 6388 . . . . . . . . . . . . . . 15 ((โˆฉ ๐‘† โˆˆ On โˆง ๐‘ง โˆˆ โˆฉ ๐‘†) โ†’ ๐‘ง โˆˆ On)
8515, 84sylan 579 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ง โˆˆ โˆฉ ๐‘†) โ†’ ๐‘ง โˆˆ On)
8685ex 412 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ง โˆˆ โˆฉ ๐‘† โ†’ ๐‘ง โˆˆ On))
8786ancrd 551 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ง โˆˆ โˆฉ ๐‘† โ†’ (๐‘ง โˆˆ On โˆง ๐‘ง โˆˆ โˆฉ ๐‘†)))
8874expimpd 453 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘ง โˆˆ On โˆง ๐‘ง โˆˆ โˆฉ ๐‘†) โ†’ (๐ถ +o ๐‘ง) โˆˆ ๐ท))
89 onelss 6405 . . . . . . . . . . . . 13 (๐ท โˆˆ On โ†’ ((๐ถ +o ๐‘ง) โˆˆ ๐ท โ†’ (๐ถ +o ๐‘ง) โІ ๐ท))
905, 89syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ถ +o ๐‘ง) โˆˆ ๐ท โ†’ (๐ถ +o ๐‘ง) โІ ๐ท))
9187, 88, 903syld 60 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ง โˆˆ โˆฉ ๐‘† โ†’ (๐ถ +o ๐‘ง) โІ ๐ท))
9291ralrimiv 3140 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘ง โˆˆ โˆฉ ๐‘†(๐ถ +o ๐‘ง) โІ ๐ท)
93 iunss 5042 . . . . . . . . . 10 (โˆช ๐‘ง โˆˆ โˆฉ ๐‘†(๐ถ +o ๐‘ง) โІ ๐ท โ†” โˆ€๐‘ง โˆˆ โˆฉ ๐‘†(๐ถ +o ๐‘ง) โІ ๐ท)
9492, 93sylibr 233 . . . . . . . . 9 (๐œ‘ โ†’ โˆช ๐‘ง โˆˆ โˆฉ ๐‘†(๐ถ +o ๐‘ง) โІ ๐ท)
9594adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†)) โ†’ โˆช ๐‘ง โˆˆ โˆฉ ๐‘†(๐ถ +o ๐‘ง) โІ ๐ท)
9683, 95eqsstrd 4016 . . . . . . 7 ((๐œ‘ โˆง (โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†)) โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท)
9796ex 412 . . . . . 6 (๐œ‘ โ†’ ((โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†) โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท))
9853, 81, 973jaod 1426 . . . . 5 (๐œ‘ โ†’ ((โˆฉ ๐‘† = โˆ… โˆจ โˆƒ๐‘ง โˆˆ On โˆฉ ๐‘† = suc ๐‘ง โˆจ (โˆฉ ๐‘† โˆˆ V โˆง Lim โˆฉ ๐‘†)) โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท))
9944, 98mpd 15 . . . 4 (๐œ‘ โ†’ (๐ถ +o โˆฉ ๐‘†) โІ ๐ท)
1004rspcev 3607 . . . . . . 7 ((๐ท โˆˆ On โˆง ๐ท โІ (๐ถ +o ๐ท)) โ†’ โˆƒ๐‘ฆ โˆˆ On ๐ท โІ (๐ถ +o ๐‘ฆ))
1015, 10, 100syl2anc 583 . . . . . 6 (๐œ‘ โ†’ โˆƒ๐‘ฆ โˆˆ On ๐ท โІ (๐ถ +o ๐‘ฆ))
102 nfcv 2898 . . . . . . . 8 โ„ฒ๐‘ฆ๐ท
103 nfcv 2898 . . . . . . . . 9 โ„ฒ๐‘ฆ๐ถ
104 nfcv 2898 . . . . . . . . 9 โ„ฒ๐‘ฆ +o
105 nfrab1 3446 . . . . . . . . . 10 โ„ฒ๐‘ฆ{๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}
106105nfint 4954 . . . . . . . . 9 โ„ฒ๐‘ฆโˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}
107103, 104, 106nfov 7444 . . . . . . . 8 โ„ฒ๐‘ฆ(๐ถ +o โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)})
108102, 107nfss 3970 . . . . . . 7 โ„ฒ๐‘ฆ ๐ท โІ (๐ถ +o โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)})
109 oveq2 7422 . . . . . . . 8 (๐‘ฆ = โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)} โ†’ (๐ถ +o ๐‘ฆ) = (๐ถ +o โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}))
110109sseq2d 4010 . . . . . . 7 (๐‘ฆ = โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)} โ†’ (๐ท โІ (๐ถ +o ๐‘ฆ) โ†” ๐ท โІ (๐ถ +o โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)})))
111108, 110onminsb 7791 . . . . . 6 (โˆƒ๐‘ฆ โˆˆ On ๐ท โІ (๐ถ +o ๐‘ฆ) โ†’ ๐ท โІ (๐ถ +o โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}))
112101, 111syl 17 . . . . 5 (๐œ‘ โ†’ ๐ท โІ (๐ถ +o โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)}))
11339oveq2i 7425 . . . . 5 (๐ถ +o โˆฉ ๐‘†) = (๐ถ +o โˆฉ {๐‘ฆ โˆˆ On โˆฃ ๐ท โІ (๐ถ +o ๐‘ฆ)})
114112, 113sseqtrrdi 4029 . . . 4 (๐œ‘ โ†’ ๐ท โІ (๐ถ +o โˆฉ ๐‘†))
11599, 114eqssd 3995 . . 3 (๐œ‘ โ†’ (๐ถ +o โˆฉ ๐‘†) = ๐ท)
116 omelon 9661 . . . . . 6 ฯ‰ โˆˆ On
117 omcl 8550 . . . . . 6 ((ฯ‰ โˆˆ On โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ ยทo ๐ท) โˆˆ On)
118116, 5, 117sylancr 586 . . . . 5 (๐œ‘ โ†’ (ฯ‰ ยทo ๐ท) โˆˆ On)
119116a1i 11 . . . . . . 7 (๐œ‘ โ†’ ฯ‰ โˆˆ On)
120 naddwordnex.n . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ ๐‘€)
121 naddwordnex.m . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ ฯ‰)
122120, 121jca 511 . . . . . . 7 (๐œ‘ โ†’ (๐‘ โˆˆ ๐‘€ โˆง ๐‘€ โˆˆ ฯ‰))
123 ontr1 6409 . . . . . . 7 (ฯ‰ โˆˆ On โ†’ ((๐‘ โˆˆ ๐‘€ โˆง ๐‘€ โˆˆ ฯ‰) โ†’ ๐‘ โˆˆ ฯ‰))
124119, 122, 123sylc 65 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ ฯ‰)
125 nnon 7870 . . . . . 6 (๐‘ โˆˆ ฯ‰ โ†’ ๐‘ โˆˆ On)
126124, 125syl 17 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ On)
127 oaword1 8566 . . . . 5 (((ฯ‰ ยทo ๐ท) โˆˆ On โˆง ๐‘ โˆˆ On) โ†’ (ฯ‰ ยทo ๐ท) โІ ((ฯ‰ ยทo ๐ท) +o ๐‘))
128118, 126, 127syl2anc 583 . . . 4 (๐œ‘ โ†’ (ฯ‰ ยทo ๐ท) โІ ((ฯ‰ ยทo ๐ท) +o ๐‘))
129 naddwordnex.a . . . . . 6 (๐œ‘ โ†’ ๐ด = ((ฯ‰ ยทo ๐ถ) +o ๐‘€))
130129oveq1d 7429 . . . . 5 (๐œ‘ โ†’ (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)) = (((ฯ‰ ยทo ๐ถ) +o ๐‘€) +o (ฯ‰ ยทo โˆฉ ๐‘†)))
131 omcl 8550 . . . . . . 7 ((ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ ยทo ๐ถ) โˆˆ On)
132116, 8, 131sylancr 586 . . . . . 6 (๐œ‘ โ†’ (ฯ‰ ยทo ๐ถ) โˆˆ On)
133 nnon 7870 . . . . . . 7 (๐‘€ โˆˆ ฯ‰ โ†’ ๐‘€ โˆˆ On)
134121, 133syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘€ โˆˆ On)
135 omcl 8550 . . . . . . 7 ((ฯ‰ โˆˆ On โˆง โˆฉ ๐‘† โˆˆ On) โ†’ (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On)
136116, 15, 135sylancr 586 . . . . . 6 (๐œ‘ โ†’ (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On)
137 oaass 8575 . . . . . 6 (((ฯ‰ ยทo ๐ถ) โˆˆ On โˆง ๐‘€ โˆˆ On โˆง (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On) โ†’ (((ฯ‰ ยทo ๐ถ) +o ๐‘€) +o (ฯ‰ ยทo โˆฉ ๐‘†)) = ((ฯ‰ ยทo ๐ถ) +o (๐‘€ +o (ฯ‰ ยทo โˆฉ ๐‘†))))
138132, 134, 136, 137syl3anc 1369 . . . . 5 (๐œ‘ โ†’ (((ฯ‰ ยทo ๐ถ) +o ๐‘€) +o (ฯ‰ ยทo โˆฉ ๐‘†)) = ((ฯ‰ ยทo ๐ถ) +o (๐‘€ +o (ฯ‰ ยทo โˆฉ ๐‘†))))
13915, 116jctil 519 . . . . . . . . 9 (๐œ‘ โ†’ (ฯ‰ โˆˆ On โˆง โˆฉ ๐‘† โˆˆ On))
140 omword1 8587 . . . . . . . . 9 (((ฯ‰ โˆˆ On โˆง โˆฉ ๐‘† โˆˆ On) โˆง โˆ… โˆˆ โˆฉ ๐‘†) โ†’ ฯ‰ โІ (ฯ‰ ยทo โˆฉ ๐‘†))
141139, 40, 140syl2anc 583 . . . . . . . 8 (๐œ‘ โ†’ ฯ‰ โІ (ฯ‰ ยทo โˆฉ ๐‘†))
142 oaabs 8662 . . . . . . . 8 (((๐‘€ โˆˆ ฯ‰ โˆง (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On) โˆง ฯ‰ โІ (ฯ‰ ยทo โˆฉ ๐‘†)) โ†’ (๐‘€ +o (ฯ‰ ยทo โˆฉ ๐‘†)) = (ฯ‰ ยทo โˆฉ ๐‘†))
143121, 136, 141, 142syl21anc 837 . . . . . . 7 (๐œ‘ โ†’ (๐‘€ +o (ฯ‰ ยทo โˆฉ ๐‘†)) = (ฯ‰ ยทo โˆฉ ๐‘†))
144143oveq2d 7430 . . . . . 6 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ถ) +o (๐‘€ +o (ฯ‰ ยทo โˆฉ ๐‘†))) = ((ฯ‰ ยทo ๐ถ) +o (ฯ‰ ยทo โˆฉ ๐‘†)))
145 odi 8593 . . . . . . 7 ((ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On โˆง โˆฉ ๐‘† โˆˆ On) โ†’ (ฯ‰ ยทo (๐ถ +o โˆฉ ๐‘†)) = ((ฯ‰ ยทo ๐ถ) +o (ฯ‰ ยทo โˆฉ ๐‘†)))
146119, 8, 15, 145syl3anc 1369 . . . . . 6 (๐œ‘ โ†’ (ฯ‰ ยทo (๐ถ +o โˆฉ ๐‘†)) = ((ฯ‰ ยทo ๐ถ) +o (ฯ‰ ยทo โˆฉ ๐‘†)))
147115oveq2d 7430 . . . . . 6 (๐œ‘ โ†’ (ฯ‰ ยทo (๐ถ +o โˆฉ ๐‘†)) = (ฯ‰ ยทo ๐ท))
148144, 146, 1473eqtr2d 2773 . . . . 5 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ถ) +o (๐‘€ +o (ฯ‰ ยทo โˆฉ ๐‘†))) = (ฯ‰ ยทo ๐ท))
149130, 138, 1483eqtrd 2771 . . . 4 (๐œ‘ โ†’ (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)) = (ฯ‰ ยทo ๐ท))
150 naddwordnex.b . . . 4 (๐œ‘ โ†’ ๐ต = ((ฯ‰ ยทo ๐ท) +o ๐‘))
151128, 149, 1503sstr4d 4025 . . 3 (๐œ‘ โ†’ (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)) โІ ๐ต)
152 naddcl 8691 . . . . . . . 8 (((ฯ‰ ยทo ๐ถ) โˆˆ On โˆง (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On) โ†’ ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) โˆˆ On)
153132, 136, 152syl2anc 583 . . . . . . 7 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) โˆˆ On)
154118, 153, 1343jca 1126 . . . . . 6 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ท) โˆˆ On โˆง ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) โˆˆ On โˆง ๐‘€ โˆˆ On))
155147, 146eqtr3d 2769 . . . . . . 7 (๐œ‘ โ†’ (ฯ‰ ยทo ๐ท) = ((ฯ‰ ยทo ๐ถ) +o (ฯ‰ ยทo โˆฉ ๐‘†)))
156 naddgeoa 42747 . . . . . . . 8 (((ฯ‰ ยทo ๐ถ) โˆˆ On โˆง (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On) โ†’ ((ฯ‰ ยทo ๐ถ) +o (ฯ‰ ยทo โˆฉ ๐‘†)) โІ ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)))
157132, 136, 156syl2anc 583 . . . . . . 7 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ถ) +o (ฯ‰ ยทo โˆฉ ๐‘†)) โІ ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)))
158155, 157eqsstrd 4016 . . . . . 6 (๐œ‘ โ†’ (ฯ‰ ยทo ๐ท) โІ ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)))
159 oawordri 8564 . . . . . 6 (((ฯ‰ ยทo ๐ท) โˆˆ On โˆง ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) โˆˆ On โˆง ๐‘€ โˆˆ On) โ†’ ((ฯ‰ ยทo ๐ท) โІ ((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) โ†’ ((ฯ‰ ยทo ๐ท) +o ๐‘€) โІ (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +o ๐‘€)))
160154, 158, 159sylc 65 . . . . 5 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ท) +o ๐‘€) โІ (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +o ๐‘€))
161 naddonnn 42748 . . . . . . . . 9 (((ฯ‰ ยทo ๐ถ) โˆˆ On โˆง ๐‘€ โˆˆ ฯ‰) โ†’ ((ฯ‰ ยทo ๐ถ) +o ๐‘€) = ((ฯ‰ ยทo ๐ถ) +no ๐‘€))
162132, 121, 161syl2anc 583 . . . . . . . 8 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ถ) +o ๐‘€) = ((ฯ‰ ยทo ๐ถ) +no ๐‘€))
163129, 162eqtrd 2767 . . . . . . 7 (๐œ‘ โ†’ ๐ด = ((ฯ‰ ยทo ๐ถ) +no ๐‘€))
164163oveq1d 7429 . . . . . 6 (๐œ‘ โ†’ (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†)) = (((ฯ‰ ยทo ๐ถ) +no ๐‘€) +no (ฯ‰ ยทo โˆฉ ๐‘†)))
165 naddass 8710 . . . . . . . 8 (((ฯ‰ ยทo ๐ถ) โˆˆ On โˆง ๐‘€ โˆˆ On โˆง (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On) โ†’ (((ฯ‰ ยทo ๐ถ) +no ๐‘€) +no (ฯ‰ ยทo โˆฉ ๐‘†)) = ((ฯ‰ ยทo ๐ถ) +no (๐‘€ +no (ฯ‰ ยทo โˆฉ ๐‘†))))
166132, 134, 136, 165syl3anc 1369 . . . . . . 7 (๐œ‘ โ†’ (((ฯ‰ ยทo ๐ถ) +no ๐‘€) +no (ฯ‰ ยทo โˆฉ ๐‘†)) = ((ฯ‰ ยทo ๐ถ) +no (๐‘€ +no (ฯ‰ ยทo โˆฉ ๐‘†))))
167 naddcom 8696 . . . . . . . . 9 ((๐‘€ โˆˆ On โˆง (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On) โ†’ (๐‘€ +no (ฯ‰ ยทo โˆฉ ๐‘†)) = ((ฯ‰ ยทo โˆฉ ๐‘†) +no ๐‘€))
168134, 136, 167syl2anc 583 . . . . . . . 8 (๐œ‘ โ†’ (๐‘€ +no (ฯ‰ ยทo โˆฉ ๐‘†)) = ((ฯ‰ ยทo โˆฉ ๐‘†) +no ๐‘€))
169168oveq2d 7430 . . . . . . 7 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ถ) +no (๐‘€ +no (ฯ‰ ยทo โˆฉ ๐‘†))) = ((ฯ‰ ยทo ๐ถ) +no ((ฯ‰ ยทo โˆฉ ๐‘†) +no ๐‘€)))
170 naddonnn 42748 . . . . . . . . 9 ((((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) โˆˆ On โˆง ๐‘€ โˆˆ ฯ‰) โ†’ (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +o ๐‘€) = (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +no ๐‘€))
171153, 121, 170syl2anc 583 . . . . . . . 8 (๐œ‘ โ†’ (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +o ๐‘€) = (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +no ๐‘€))
172 naddass 8710 . . . . . . . . 9 (((ฯ‰ ยทo ๐ถ) โˆˆ On โˆง (ฯ‰ ยทo โˆฉ ๐‘†) โˆˆ On โˆง ๐‘€ โˆˆ On) โ†’ (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +no ๐‘€) = ((ฯ‰ ยทo ๐ถ) +no ((ฯ‰ ยทo โˆฉ ๐‘†) +no ๐‘€)))
173132, 136, 134, 172syl3anc 1369 . . . . . . . 8 (๐œ‘ โ†’ (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +no ๐‘€) = ((ฯ‰ ยทo ๐ถ) +no ((ฯ‰ ยทo โˆฉ ๐‘†) +no ๐‘€)))
174171, 173eqtr2d 2768 . . . . . . 7 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ถ) +no ((ฯ‰ ยทo โˆฉ ๐‘†) +no ๐‘€)) = (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +o ๐‘€))
175166, 169, 1743eqtrd 2771 . . . . . 6 (๐œ‘ โ†’ (((ฯ‰ ยทo ๐ถ) +no ๐‘€) +no (ฯ‰ ยทo โˆฉ ๐‘†)) = (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +o ๐‘€))
176164, 175eqtr2d 2768 . . . . 5 (๐œ‘ โ†’ (((ฯ‰ ยทo ๐ถ) +no (ฯ‰ ยทo โˆฉ ๐‘†)) +o ๐‘€) = (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†)))
177160, 176sseqtrd 4018 . . . 4 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ท) +o ๐‘€) โІ (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†)))
178134, 118jca 511 . . . . . 6 (๐œ‘ โ†’ (๐‘€ โˆˆ On โˆง (ฯ‰ ยทo ๐ท) โˆˆ On))
179 oaordi 8560 . . . . . 6 ((๐‘€ โˆˆ On โˆง (ฯ‰ ยทo ๐ท) โˆˆ On) โ†’ (๐‘ โˆˆ ๐‘€ โ†’ ((ฯ‰ ยทo ๐ท) +o ๐‘) โˆˆ ((ฯ‰ ยทo ๐ท) +o ๐‘€)))
180178, 120, 179sylc 65 . . . . 5 (๐œ‘ โ†’ ((ฯ‰ ยทo ๐ท) +o ๐‘) โˆˆ ((ฯ‰ ยทo ๐ท) +o ๐‘€))
181150, 180eqeltrd 2828 . . . 4 (๐œ‘ โ†’ ๐ต โˆˆ ((ฯ‰ ยทo ๐ท) +o ๐‘€))
182177, 181sseldd 3979 . . 3 (๐œ‘ โ†’ ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†)))
183115, 151, 1823jca 1126 . 2 (๐œ‘ โ†’ ((๐ถ +o โˆฉ ๐‘†) = ๐ท โˆง (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)) โІ ๐ต โˆง ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†))))
184 oveq2 7422 . . . . 5 (๐‘ฅ = โˆฉ ๐‘† โ†’ (๐ถ +o ๐‘ฅ) = (๐ถ +o โˆฉ ๐‘†))
185184eqeq1d 2729 . . . 4 (๐‘ฅ = โˆฉ ๐‘† โ†’ ((๐ถ +o ๐‘ฅ) = ๐ท โ†” (๐ถ +o โˆฉ ๐‘†) = ๐ท))
186 oveq2 7422 . . . . . 6 (๐‘ฅ = โˆฉ ๐‘† โ†’ (ฯ‰ ยทo ๐‘ฅ) = (ฯ‰ ยทo โˆฉ ๐‘†))
187186oveq2d 7430 . . . . 5 (๐‘ฅ = โˆฉ ๐‘† โ†’ (๐ด +o (ฯ‰ ยทo ๐‘ฅ)) = (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)))
188187sseq1d 4009 . . . 4 (๐‘ฅ = โˆฉ ๐‘† โ†’ ((๐ด +o (ฯ‰ ยทo ๐‘ฅ)) โІ ๐ต โ†” (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)) โІ ๐ต))
189186oveq2d 7430 . . . . 5 (๐‘ฅ = โˆฉ ๐‘† โ†’ (๐ด +no (ฯ‰ ยทo ๐‘ฅ)) = (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†)))
190189eleq2d 2814 . . . 4 (๐‘ฅ = โˆฉ ๐‘† โ†’ (๐ต โˆˆ (๐ด +no (ฯ‰ ยทo ๐‘ฅ)) โ†” ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†))))
191185, 188, 1903anbi123d 1433 . . 3 (๐‘ฅ = โˆฉ ๐‘† โ†’ (((๐ถ +o ๐‘ฅ) = ๐ท โˆง (๐ด +o (ฯ‰ ยทo ๐‘ฅ)) โІ ๐ต โˆง ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo ๐‘ฅ))) โ†” ((๐ถ +o โˆฉ ๐‘†) = ๐ท โˆง (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)) โІ ๐ต โˆง ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†)))))
192191rspcev 3607 . 2 ((โˆฉ ๐‘† โˆˆ (On โˆ– 1o) โˆง ((๐ถ +o โˆฉ ๐‘†) = ๐ท โˆง (๐ด +o (ฯ‰ ยทo โˆฉ ๐‘†)) โІ ๐ต โˆง ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo โˆฉ ๐‘†)))) โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)((๐ถ +o ๐‘ฅ) = ๐ท โˆง (๐ด +o (ฯ‰ ยทo ๐‘ฅ)) โІ ๐ต โˆง ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo ๐‘ฅ))))
19342, 183, 192syl2anc 583 1 (๐œ‘ โ†’ โˆƒ๐‘ฅ โˆˆ (On โˆ– 1o)((๐ถ +o ๐‘ฅ) = ๐ท โˆง (๐ด +o (ฯ‰ ยทo ๐‘ฅ)) โІ ๐ต โˆง ๐ต โˆˆ (๐ด +no (ฯ‰ ยทo ๐‘ฅ))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ w3o 1084   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2935  โˆ€wral 3056  โˆƒwrex 3065  {crab 3427  Vcvv 3469   โˆ– cdif 3941   โІ wss 3944  โˆ…c0 4318  โˆฉ cint 4944  โˆช ciun 4991  Oncon0 6363  Lim wlim 6364  suc csuc 6365  (class class class)co 7414  ฯ‰com 7864  1oc1o 8473   +o coa 8477   ยทo comu 8478   +no cnadd 8679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-ot 4633  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-omul 8485  df-nadd 8680
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator