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

Theorem oeeui 8554
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 8555 gives an explicit expression for the unique solution of the equation, in terms of the solution ๐‘ƒ to omeu 8537.) (Contributed by Mario Carneiro, 25-May-2015.)
Hypotheses
Ref Expression
oeeu.1 ๐‘‹ = โˆช โˆฉ {๐‘ฅ โˆˆ On โˆฃ ๐ต โˆˆ (๐ด โ†‘o ๐‘ฅ)}
oeeu.2 ๐‘ƒ = (โ„ฉ๐‘คโˆƒ๐‘ฆ โˆˆ On โˆƒ๐‘ง โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘ค = โŸจ๐‘ฆ, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ต))
oeeu.3 ๐‘Œ = (1st โ€˜๐‘ƒ)
oeeu.4 ๐‘ = (2nd โ€˜๐‘ƒ)
Assertion
Ref Expression
oeeui ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o) โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐ถ)) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” (๐ถ = ๐‘‹ โˆง ๐ท = ๐‘Œ โˆง ๐ธ = ๐‘)))
Distinct variable groups:   ๐‘ฅ,๐‘ค,๐‘ฆ,๐‘ง,๐ด   ๐‘ค,๐ต,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘ค,๐‘‹,๐‘ฆ,๐‘ง
Allowed substitution hints:   ๐ถ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐ท(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘ƒ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐ธ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘‹(๐‘ฅ)   ๐‘Œ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)

Proof of Theorem oeeui
Dummy variables ๐‘Ž ๐‘‘ ๐‘’ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 4091 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ (On โˆ– 2o) โ†’ ๐ด โˆˆ On)
21adantr 482 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ ๐ด โˆˆ On)
32ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ด โˆˆ On)
4 simprl 770 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ถ โˆˆ On)
5 oecl 8488 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (๐ด โ†‘o ๐ถ) โˆˆ On)
63, 4, 5syl2anc 585 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o ๐ถ) โˆˆ On)
7 om1 8494 . . . . . . . . . . . . . . 15 ((๐ด โ†‘o ๐ถ) โˆˆ On โ†’ ((๐ด โ†‘o ๐ถ) ยทo 1o) = (๐ด โ†‘o ๐ถ))
86, 7syl 17 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo 1o) = (๐ด โ†‘o ๐ถ))
9 df1o2 8424 . . . . . . . . . . . . . . . 16 1o = {โˆ…}
10 dif1o 8451 . . . . . . . . . . . . . . . . . . . 20 (๐ท โˆˆ (๐ด โˆ– 1o) โ†” (๐ท โˆˆ ๐ด โˆง ๐ท โ‰  โˆ…))
1110simprbi 498 . . . . . . . . . . . . . . . . . . 19 (๐ท โˆˆ (๐ด โˆ– 1o) โ†’ ๐ท โ‰  โˆ…)
1211ad2antll 728 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ท โ‰  โˆ…)
13 eldifi 4091 . . . . . . . . . . . . . . . . . . . . 21 (๐ท โˆˆ (๐ด โˆ– 1o) โ†’ ๐ท โˆˆ ๐ด)
1413ad2antll 728 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ท โˆˆ ๐ด)
15 onelon 6347 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ On โˆง ๐ท โˆˆ ๐ด) โ†’ ๐ท โˆˆ On)
163, 14, 15syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ท โˆˆ On)
17 on0eln0 6378 . . . . . . . . . . . . . . . . . . 19 (๐ท โˆˆ On โ†’ (โˆ… โˆˆ ๐ท โ†” ๐ท โ‰  โˆ…))
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (โˆ… โˆˆ ๐ท โ†” ๐ท โ‰  โˆ…))
1912, 18mpbird 257 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ โˆ… โˆˆ ๐ท)
2019snssd 4774 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ {โˆ…} โŠ† ๐ท)
219, 20eqsstrid 3997 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ 1o โŠ† ๐ท)
22 1on 8429 . . . . . . . . . . . . . . . . 17 1o โˆˆ On
2322a1i 11 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ 1o โˆˆ On)
24 omwordi 8523 . . . . . . . . . . . . . . . 16 ((1o โˆˆ On โˆง ๐ท โˆˆ On โˆง (๐ด โ†‘o ๐ถ) โˆˆ On) โ†’ (1o โŠ† ๐ท โ†’ ((๐ด โ†‘o ๐ถ) ยทo 1o) โŠ† ((๐ด โ†‘o ๐ถ) ยทo ๐ท)))
2523, 16, 6, 24syl3anc 1372 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (1o โŠ† ๐ท โ†’ ((๐ด โ†‘o ๐ถ) ยทo 1o) โŠ† ((๐ด โ†‘o ๐ถ) ยทo ๐ท)))
2621, 25mpd 15 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo 1o) โŠ† ((๐ด โ†‘o ๐ถ) ยทo ๐ท))
278, 26eqsstrrd 3988 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o ๐ถ) โŠ† ((๐ด โ†‘o ๐ถ) ยทo ๐ท))
28 omcl 8487 . . . . . . . . . . . . . . . 16 (((๐ด โ†‘o ๐ถ) โˆˆ On โˆง ๐ท โˆˆ On) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ On)
296, 16, 28syl2anc 585 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ On)
30 simplrl 776 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ธ โˆˆ (๐ด โ†‘o ๐ถ))
31 onelon 6347 . . . . . . . . . . . . . . . 16 (((๐ด โ†‘o ๐ถ) โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐ถ)) โ†’ ๐ธ โˆˆ On)
326, 30, 31syl2anc 585 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ธ โˆˆ On)
33 oaword1 8504 . . . . . . . . . . . . . . 15 ((((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ On โˆง ๐ธ โˆˆ On) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โŠ† (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ))
3429, 32, 33syl2anc 585 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โŠ† (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ))
35 simplrr 777 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)
3634, 35sseqtrd 3989 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โŠ† ๐ต)
3727, 36sstrd 3959 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o ๐ถ) โŠ† ๐ต)
38 oeeu.1 . . . . . . . . . . . . . . 15 ๐‘‹ = โˆช โˆฉ {๐‘ฅ โˆˆ On โˆฃ ๐ต โˆˆ (๐ด โ†‘o ๐‘ฅ)}
3938oeeulem 8553 . . . . . . . . . . . . . 14 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (๐‘‹ โˆˆ On โˆง (๐ด โ†‘o ๐‘‹) โŠ† ๐ต โˆง ๐ต โˆˆ (๐ด โ†‘o suc ๐‘‹)))
4039simp3d 1145 . . . . . . . . . . . . 13 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ ๐ต โˆˆ (๐ด โ†‘o suc ๐‘‹))
4140ad2antrr 725 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ต โˆˆ (๐ด โ†‘o suc ๐‘‹))
4239simp1d 1143 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ ๐‘‹ โˆˆ On)
4342ad2antrr 725 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐‘‹ โˆˆ On)
44 onsuc 7751 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ On โ†’ suc ๐‘‹ โˆˆ On)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ suc ๐‘‹ โˆˆ On)
46 oecl 8488 . . . . . . . . . . . . . 14 ((๐ด โˆˆ On โˆง suc ๐‘‹ โˆˆ On) โ†’ (๐ด โ†‘o suc ๐‘‹) โˆˆ On)
473, 45, 46syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o suc ๐‘‹) โˆˆ On)
48 ontr2 6369 . . . . . . . . . . . . 13 (((๐ด โ†‘o ๐ถ) โˆˆ On โˆง (๐ด โ†‘o suc ๐‘‹) โˆˆ On) โ†’ (((๐ด โ†‘o ๐ถ) โŠ† ๐ต โˆง ๐ต โˆˆ (๐ด โ†‘o suc ๐‘‹)) โ†’ (๐ด โ†‘o ๐ถ) โˆˆ (๐ด โ†‘o suc ๐‘‹)))
496, 47, 48syl2anc 585 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (((๐ด โ†‘o ๐ถ) โŠ† ๐ต โˆง ๐ต โˆˆ (๐ด โ†‘o suc ๐‘‹)) โ†’ (๐ด โ†‘o ๐ถ) โˆˆ (๐ด โ†‘o suc ๐‘‹)))
5037, 41, 49mp2and 698 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o ๐ถ) โˆˆ (๐ด โ†‘o suc ๐‘‹))
51 simplll 774 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ด โˆˆ (On โˆ– 2o))
52 oeord 8540 . . . . . . . . . . . 12 ((๐ถ โˆˆ On โˆง suc ๐‘‹ โˆˆ On โˆง ๐ด โˆˆ (On โˆ– 2o)) โ†’ (๐ถ โˆˆ suc ๐‘‹ โ†” (๐ด โ†‘o ๐ถ) โˆˆ (๐ด โ†‘o suc ๐‘‹)))
534, 45, 51, 52syl3anc 1372 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ถ โˆˆ suc ๐‘‹ โ†” (๐ด โ†‘o ๐ถ) โˆˆ (๐ด โ†‘o suc ๐‘‹)))
5450, 53mpbird 257 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ถ โˆˆ suc ๐‘‹)
55 onsssuc 6412 . . . . . . . . . . 11 ((๐ถ โˆˆ On โˆง ๐‘‹ โˆˆ On) โ†’ (๐ถ โŠ† ๐‘‹ โ†” ๐ถ โˆˆ suc ๐‘‹))
564, 43, 55syl2anc 585 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ถ โŠ† ๐‘‹ โ†” ๐ถ โˆˆ suc ๐‘‹))
5754, 56mpbird 257 . . . . . . . . 9 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ถ โŠ† ๐‘‹)
5839simp2d 1144 . . . . . . . . . . . . 13 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ๐ต)
5958ad2antrr 725 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ๐ต)
60 eloni 6332 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ On โ†’ Ord ๐ด)
613, 60syl 17 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ Ord ๐ด)
62 ordsucss 7758 . . . . . . . . . . . . . . . 16 (Ord ๐ด โ†’ (๐ท โˆˆ ๐ด โ†’ suc ๐ท โŠ† ๐ด))
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ suc ๐ท โŠ† ๐ด)
64 onsuc 7751 . . . . . . . . . . . . . . . . 17 (๐ท โˆˆ On โ†’ suc ๐ท โˆˆ On)
6516, 64syl 17 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ suc ๐ท โˆˆ On)
66 dif20el 8456 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ (On โˆ– 2o) โ†’ โˆ… โˆˆ ๐ด)
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ โˆ… โˆˆ ๐ด)
68 oen0 8538 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ถ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ โˆ… โˆˆ (๐ด โ†‘o ๐ถ))
693, 4, 67, 68syl21anc 837 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ โˆ… โˆˆ (๐ด โ†‘o ๐ถ))
70 omword 8522 . . . . . . . . . . . . . . . 16 (((suc ๐ท โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด โ†‘o ๐ถ) โˆˆ On) โˆง โˆ… โˆˆ (๐ด โ†‘o ๐ถ)) โ†’ (suc ๐ท โŠ† ๐ด โ†” ((๐ด โ†‘o ๐ถ) ยทo suc ๐ท) โŠ† ((๐ด โ†‘o ๐ถ) ยทo ๐ด)))
7165, 3, 6, 69, 70syl31anc 1374 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (suc ๐ท โŠ† ๐ด โ†” ((๐ด โ†‘o ๐ถ) ยทo suc ๐ท) โŠ† ((๐ด โ†‘o ๐ถ) ยทo ๐ด)))
7263, 71mpbid 231 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo suc ๐ท) โŠ† ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
73 oaord 8499 . . . . . . . . . . . . . . . . . 18 ((๐ธ โˆˆ On โˆง (๐ด โ†‘o ๐ถ) โˆˆ On โˆง ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ On) โ†’ (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โ†” (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) โˆˆ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o (๐ด โ†‘o ๐ถ))))
7432, 6, 29, 73syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โ†” (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) โˆˆ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o (๐ด โ†‘o ๐ถ))))
7530, 74mpbid 231 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) โˆˆ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o (๐ด โ†‘o ๐ถ)))
7635, 75eqeltrrd 2839 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ต โˆˆ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o (๐ด โ†‘o ๐ถ)))
77 odi 8531 . . . . . . . . . . . . . . . . 17 (((๐ด โ†‘o ๐ถ) โˆˆ On โˆง ๐ท โˆˆ On โˆง 1o โˆˆ On) โ†’ ((๐ด โ†‘o ๐ถ) ยทo (๐ท +o 1o)) = (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ((๐ด โ†‘o ๐ถ) ยทo 1o)))
786, 16, 23, 77syl3anc 1372 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo (๐ท +o 1o)) = (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ((๐ด โ†‘o ๐ถ) ยทo 1o)))
79 oa1suc 8482 . . . . . . . . . . . . . . . . . 18 (๐ท โˆˆ On โ†’ (๐ท +o 1o) = suc ๐ท)
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ท +o 1o) = suc ๐ท)
8180oveq2d 7378 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo (๐ท +o 1o)) = ((๐ด โ†‘o ๐ถ) ยทo suc ๐ท))
828oveq2d 7378 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ((๐ด โ†‘o ๐ถ) ยทo 1o)) = (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o (๐ด โ†‘o ๐ถ)))
8378, 81, 823eqtr3d 2785 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ((๐ด โ†‘o ๐ถ) ยทo suc ๐ท) = (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o (๐ด โ†‘o ๐ถ)))
8476, 83eleqtrrd 2841 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ต โˆˆ ((๐ด โ†‘o ๐ถ) ยทo suc ๐ท))
8572, 84sseldd 3950 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ต โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
86 oesuc 8478 . . . . . . . . . . . . . 14 ((๐ด โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (๐ด โ†‘o suc ๐ถ) = ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
873, 4, 86syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o suc ๐ถ) = ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
8885, 87eleqtrrd 2841 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ต โˆˆ (๐ด โ†‘o suc ๐ถ))
89 oecl 8488 . . . . . . . . . . . . . 14 ((๐ด โˆˆ On โˆง ๐‘‹ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
903, 43, 89syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
91 onsuc 7751 . . . . . . . . . . . . . . 15 (๐ถ โˆˆ On โ†’ suc ๐ถ โˆˆ On)
9291ad2antrl 727 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ suc ๐ถ โˆˆ On)
93 oecl 8488 . . . . . . . . . . . . . 14 ((๐ด โˆˆ On โˆง suc ๐ถ โˆˆ On) โ†’ (๐ด โ†‘o suc ๐ถ) โˆˆ On)
943, 92, 93syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o suc ๐ถ) โˆˆ On)
95 ontr2 6369 . . . . . . . . . . . . 13 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง (๐ด โ†‘o suc ๐ถ) โˆˆ On) โ†’ (((๐ด โ†‘o ๐‘‹) โŠ† ๐ต โˆง ๐ต โˆˆ (๐ด โ†‘o suc ๐ถ)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o suc ๐ถ)))
9690, 94, 95syl2anc 585 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (((๐ด โ†‘o ๐‘‹) โŠ† ๐ต โˆง ๐ต โˆˆ (๐ด โ†‘o suc ๐ถ)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o suc ๐ถ)))
9759, 88, 96mp2and 698 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o suc ๐ถ))
98 oeord 8540 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ On โˆง suc ๐ถ โˆˆ On โˆง ๐ด โˆˆ (On โˆ– 2o)) โ†’ (๐‘‹ โˆˆ suc ๐ถ โ†” (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o suc ๐ถ)))
9943, 92, 51, 98syl3anc 1372 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐‘‹ โˆˆ suc ๐ถ โ†” (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o suc ๐ถ)))
10097, 99mpbird 257 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐‘‹ โˆˆ suc ๐ถ)
101 onsssuc 6412 . . . . . . . . . . 11 ((๐‘‹ โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (๐‘‹ โŠ† ๐ถ โ†” ๐‘‹ โˆˆ suc ๐ถ))
10243, 4, 101syl2anc 585 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐‘‹ โŠ† ๐ถ โ†” ๐‘‹ โˆˆ suc ๐ถ))
103100, 102mpbird 257 . . . . . . . . 9 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐‘‹ โŠ† ๐ถ)
10457, 103eqssd 3966 . . . . . . . 8 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ ๐ถ = ๐‘‹)
105104, 16jca 513 . . . . . . 7 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o))) โ†’ (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On))
106 simprl 770 . . . . . . . . 9 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ถ = ๐‘‹)
10742ad2antrr 725 . . . . . . . . 9 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐‘‹ โˆˆ On)
108106, 107eqeltrd 2838 . . . . . . . 8 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ถ โˆˆ On)
1092ad2antrr 725 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ด โˆˆ On)
110109, 108, 5syl2anc 585 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ด โ†‘o ๐ถ) โˆˆ On)
111 simprr 772 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ท โˆˆ On)
112110, 111, 28syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ On)
113 simplrl 776 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ธ โˆˆ (๐ด โ†‘o ๐ถ))
114110, 113, 31syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ธ โˆˆ On)
115112, 114, 33syl2anc 585 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โŠ† (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ))
116 simplrr 777 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)
117115, 116sseqtrd 3989 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โŠ† ๐ต)
11840ad2antrr 725 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ (๐ด โ†‘o suc ๐‘‹))
119 suceq 6388 . . . . . . . . . . . . . . 15 (๐ถ = ๐‘‹ โ†’ suc ๐ถ = suc ๐‘‹)
120119ad2antrl 727 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ suc ๐ถ = suc ๐‘‹)
121120oveq2d 7378 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ด โ†‘o suc ๐ถ) = (๐ด โ†‘o suc ๐‘‹))
122109, 108, 86syl2anc 585 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ด โ†‘o suc ๐ถ) = ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
123121, 122eqtr3d 2779 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ด โ†‘o suc ๐‘‹) = ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
124118, 123eleqtrd 2840 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
125 omcl 8487 . . . . . . . . . . . . 13 (((๐ด โ†‘o ๐ถ) โˆˆ On โˆง ๐ด โˆˆ On) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ด) โˆˆ On)
126110, 109, 125syl2anc 585 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ด) โˆˆ On)
127 ontr2 6369 . . . . . . . . . . . 12 ((((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ On โˆง ((๐ด โ†‘o ๐ถ) ยทo ๐ด) โˆˆ On) โ†’ ((((๐ด โ†‘o ๐ถ) ยทo ๐ท) โŠ† ๐ต โˆง ๐ต โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด)))
128112, 126, 127syl2anc 585 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((((๐ด โ†‘o ๐ถ) ยทo ๐ท) โŠ† ๐ต โˆง ๐ต โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด)))
129117, 124, 128mp2and 698 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด))
13066adantr 482 . . . . . . . . . . . . 13 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ โˆ… โˆˆ ๐ด)
131130ad2antrr 725 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ โˆ… โˆˆ ๐ด)
132109, 108, 131, 68syl21anc 837 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ โˆ… โˆˆ (๐ด โ†‘o ๐ถ))
133 omord2 8519 . . . . . . . . . . 11 (((๐ท โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด โ†‘o ๐ถ) โˆˆ On) โˆง โˆ… โˆˆ (๐ด โ†‘o ๐ถ)) โ†’ (๐ท โˆˆ ๐ด โ†” ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด)))
134111, 109, 110, 132, 133syl31anc 1374 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ท โˆˆ ๐ด โ†” ((๐ด โ†‘o ๐ถ) ยทo ๐ท) โˆˆ ((๐ด โ†‘o ๐ถ) ยทo ๐ด)))
135129, 134mpbird 257 . . . . . . . . 9 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ท โˆˆ ๐ด)
136106oveq2d 7378 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ด โ†‘o ๐ถ) = (๐ด โ†‘o ๐‘‹))
13758ad2antrr 725 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ๐ต)
138136, 137eqsstrd 3987 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ด โ†‘o ๐ถ) โŠ† ๐ต)
139 eldifi 4091 . . . . . . . . . . . . . 14 (๐ต โˆˆ (On โˆ– 1o) โ†’ ๐ต โˆˆ On)
140139adantl 483 . . . . . . . . . . . . 13 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ ๐ต โˆˆ On)
141140ad2antrr 725 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ On)
142 ontri1 6356 . . . . . . . . . . . 12 (((๐ด โ†‘o ๐ถ) โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด โ†‘o ๐ถ) โŠ† ๐ต โ†” ยฌ ๐ต โˆˆ (๐ด โ†‘o ๐ถ)))
143110, 141, 142syl2anc 585 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((๐ด โ†‘o ๐ถ) โŠ† ๐ต โ†” ยฌ ๐ต โˆˆ (๐ด โ†‘o ๐ถ)))
144138, 143mpbid 231 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ยฌ ๐ต โˆˆ (๐ด โ†‘o ๐ถ))
145 om0 8468 . . . . . . . . . . . . . . . . 17 ((๐ด โ†‘o ๐ถ) โˆˆ On โ†’ ((๐ด โ†‘o ๐ถ) ยทo โˆ…) = โˆ…)
146110, 145syl 17 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((๐ด โ†‘o ๐ถ) ยทo โˆ…) = โˆ…)
147146oveq1d 7377 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (((๐ด โ†‘o ๐ถ) ยทo โˆ…) +o ๐ธ) = (โˆ… +o ๐ธ))
148 oa0r 8489 . . . . . . . . . . . . . . . 16 (๐ธ โˆˆ On โ†’ (โˆ… +o ๐ธ) = ๐ธ)
149114, 148syl 17 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (โˆ… +o ๐ธ) = ๐ธ)
150147, 149eqtrd 2777 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (((๐ด โ†‘o ๐ถ) ยทo โˆ…) +o ๐ธ) = ๐ธ)
151150, 113eqeltrd 2838 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (((๐ด โ†‘o ๐ถ) ยทo โˆ…) +o ๐ธ) โˆˆ (๐ด โ†‘o ๐ถ))
152 oveq2 7370 . . . . . . . . . . . . . . 15 (๐ท = โˆ… โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) = ((๐ด โ†‘o ๐ถ) ยทo โˆ…))
153152oveq1d 7377 . . . . . . . . . . . . . 14 (๐ท = โˆ… โ†’ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = (((๐ด โ†‘o ๐ถ) ยทo โˆ…) +o ๐ธ))
154153eleq1d 2823 . . . . . . . . . . . . 13 (๐ท = โˆ… โ†’ ((((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) โˆˆ (๐ด โ†‘o ๐ถ) โ†” (((๐ด โ†‘o ๐ถ) ยทo โˆ…) +o ๐ธ) โˆˆ (๐ด โ†‘o ๐ถ)))
155151, 154syl5ibrcom 247 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ท = โˆ… โ†’ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) โˆˆ (๐ด โ†‘o ๐ถ)))
156116eleq1d 2823 . . . . . . . . . . . 12 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ((((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) โˆˆ (๐ด โ†‘o ๐ถ) โ†” ๐ต โˆˆ (๐ด โ†‘o ๐ถ)))
157155, 156sylibd 238 . . . . . . . . . . 11 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ท = โˆ… โ†’ ๐ต โˆˆ (๐ด โ†‘o ๐ถ)))
158157necon3bd 2958 . . . . . . . . . 10 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (ยฌ ๐ต โˆˆ (๐ด โ†‘o ๐ถ) โ†’ ๐ท โ‰  โˆ…))
159144, 158mpd 15 . . . . . . . . 9 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ท โ‰  โˆ…)
160135, 159, 10sylanbrc 584 . . . . . . . 8 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ ๐ท โˆˆ (๐ด โˆ– 1o))
161108, 160jca 513 . . . . . . 7 ((((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โˆง (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)) โ†’ (๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o)))
162105, 161impbida 800 . . . . . 6 (((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ†’ ((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o)) โ†” (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On)))
163162ex 414 . . . . 5 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ ((๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†’ ((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o)) โ†” (๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On))))
164163pm5.32rd 579 . . . 4 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ†” ((๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต))))
165 anass 470 . . . 4 (((๐ถ = ๐‘‹ โˆง ๐ท โˆˆ On) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ†” (๐ถ = ๐‘‹ โˆง (๐ท โˆˆ On โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต))))
166164, 165bitrdi 287 . . 3 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ†” (๐ถ = ๐‘‹ โˆง (๐ท โˆˆ On โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)))))
167 3anass 1096 . . . . . 6 ((๐ท โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” (๐ท โˆˆ On โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)))
168 oveq2 7370 . . . . . . . 8 (๐ถ = ๐‘‹ โ†’ (๐ด โ†‘o ๐ถ) = (๐ด โ†‘o ๐‘‹))
169168eleq2d 2824 . . . . . . 7 (๐ถ = ๐‘‹ โ†’ (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โ†” ๐ธ โˆˆ (๐ด โ†‘o ๐‘‹)))
170168oveq1d 7377 . . . . . . . . 9 (๐ถ = ๐‘‹ โ†’ ((๐ด โ†‘o ๐ถ) ยทo ๐ท) = ((๐ด โ†‘o ๐‘‹) ยทo ๐ท))
171170oveq1d 7377 . . . . . . . 8 (๐ถ = ๐‘‹ โ†’ (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ))
172171eqeq1d 2739 . . . . . . 7 (๐ถ = ๐‘‹ โ†’ ((((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต โ†” (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ) = ๐ต))
173169, 1723anbi23d 1440 . . . . . 6 (๐ถ = ๐‘‹ โ†’ ((๐ท โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” (๐ท โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐‘‹) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ) = ๐ต)))
174167, 173bitr3id 285 . . . . 5 (๐ถ = ๐‘‹ โ†’ ((๐ท โˆˆ On โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ†” (๐ท โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐‘‹) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ) = ๐ต)))
1752, 42, 89syl2anc 585 . . . . . 6 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
176 oen0 8538 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐‘‹ โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ โˆ… โˆˆ (๐ด โ†‘o ๐‘‹))
1772, 42, 130, 176syl21anc 837 . . . . . . 7 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ โˆ… โˆˆ (๐ด โ†‘o ๐‘‹))
178177ne0d 4300 . . . . . 6 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (๐ด โ†‘o ๐‘‹) โ‰  โˆ…)
179 omeu 8537 . . . . . . 7 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐ต โˆˆ On โˆง (๐ด โ†‘o ๐‘‹) โ‰  โˆ…) โ†’ โˆƒ!๐‘Žโˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต))
180 oeeu.2 . . . . . . . . 9 ๐‘ƒ = (โ„ฉ๐‘คโˆƒ๐‘ฆ โˆˆ On โˆƒ๐‘ง โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘ค = โŸจ๐‘ฆ, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ต))
181 opeq1 4835 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘‘ โ†’ โŸจ๐‘ฆ, ๐‘งโŸฉ = โŸจ๐‘‘, ๐‘งโŸฉ)
182181eqeq2d 2748 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘‘ โ†’ (๐‘ค = โŸจ๐‘ฆ, ๐‘งโŸฉ โ†” ๐‘ค = โŸจ๐‘‘, ๐‘งโŸฉ))
183 oveq2 7370 . . . . . . . . . . . . . . 15 (๐‘ฆ = ๐‘‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) = ((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘))
184183oveq1d 7377 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘‘ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘ง))
185184eqeq1d 2739 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘‘ โ†’ ((((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ต โ†” (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘ง) = ๐ต))
186182, 185anbi12d 632 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘‘ โ†’ ((๐‘ค = โŸจ๐‘ฆ, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ต) โ†” (๐‘ค = โŸจ๐‘‘, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘ง) = ๐ต)))
187 opeq2 4836 . . . . . . . . . . . . . 14 (๐‘ง = ๐‘’ โ†’ โŸจ๐‘‘, ๐‘งโŸฉ = โŸจ๐‘‘, ๐‘’โŸฉ)
188187eqeq2d 2748 . . . . . . . . . . . . 13 (๐‘ง = ๐‘’ โ†’ (๐‘ค = โŸจ๐‘‘, ๐‘งโŸฉ โ†” ๐‘ค = โŸจ๐‘‘, ๐‘’โŸฉ))
189 oveq2 7370 . . . . . . . . . . . . . 14 (๐‘ง = ๐‘’ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘ง) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’))
190189eqeq1d 2739 . . . . . . . . . . . . 13 (๐‘ง = ๐‘’ โ†’ ((((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘ง) = ๐ต โ†” (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต))
191188, 190anbi12d 632 . . . . . . . . . . . 12 (๐‘ง = ๐‘’ โ†’ ((๐‘ค = โŸจ๐‘‘, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘ง) = ๐ต) โ†” (๐‘ค = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต)))
192186, 191cbvrex2vw 3231 . . . . . . . . . . 11 (โˆƒ๐‘ฆ โˆˆ On โˆƒ๐‘ง โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘ค = โŸจ๐‘ฆ, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ต) โ†” โˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘ค = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต))
193 eqeq1 2741 . . . . . . . . . . . . 13 (๐‘ค = ๐‘Ž โ†’ (๐‘ค = โŸจ๐‘‘, ๐‘’โŸฉ โ†” ๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ))
194193anbi1d 631 . . . . . . . . . . . 12 (๐‘ค = ๐‘Ž โ†’ ((๐‘ค = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต) โ†” (๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต)))
1951942rexbidv 3214 . . . . . . . . . . 11 (๐‘ค = ๐‘Ž โ†’ (โˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘ค = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต) โ†” โˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต)))
196192, 195bitrid 283 . . . . . . . . . 10 (๐‘ค = ๐‘Ž โ†’ (โˆƒ๐‘ฆ โˆˆ On โˆƒ๐‘ง โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘ค = โŸจ๐‘ฆ, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ต) โ†” โˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต)))
197196cbviotavw 6461 . . . . . . . . 9 (โ„ฉ๐‘คโˆƒ๐‘ฆ โˆˆ On โˆƒ๐‘ง โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘ค = โŸจ๐‘ฆ, ๐‘งโŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ต)) = (โ„ฉ๐‘Žโˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต))
198180, 197eqtri 2765 . . . . . . . 8 ๐‘ƒ = (โ„ฉ๐‘Žโˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต))
199 oeeu.3 . . . . . . . 8 ๐‘Œ = (1st โ€˜๐‘ƒ)
200 oeeu.4 . . . . . . . 8 ๐‘ = (2nd โ€˜๐‘ƒ)
201 oveq2 7370 . . . . . . . . . 10 (๐‘‘ = ๐ท โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) = ((๐ด โ†‘o ๐‘‹) ยทo ๐ท))
202201oveq1d 7377 . . . . . . . . 9 (๐‘‘ = ๐ท โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐‘’))
203202eqeq1d 2739 . . . . . . . 8 (๐‘‘ = ๐ท โ†’ ((((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต โ†” (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐‘’) = ๐ต))
204 oveq2 7370 . . . . . . . . 9 (๐‘’ = ๐ธ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐‘’) = (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ))
205204eqeq1d 2739 . . . . . . . 8 (๐‘’ = ๐ธ โ†’ ((((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐‘’) = ๐ต โ†” (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ) = ๐ต))
206198, 199, 200, 203, 205opiota 7996 . . . . . . 7 (โˆƒ!๐‘Žโˆƒ๐‘‘ โˆˆ On โˆƒ๐‘’ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘Ž = โŸจ๐‘‘, ๐‘’โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘‘) +o ๐‘’) = ๐ต) โ†’ ((๐ท โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐‘‹) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” (๐ท = ๐‘Œ โˆง ๐ธ = ๐‘)))
207179, 206syl 17 . . . . . 6 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐ต โˆˆ On โˆง (๐ด โ†‘o ๐‘‹) โ‰  โˆ…) โ†’ ((๐ท โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐‘‹) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” (๐ท = ๐‘Œ โˆง ๐ธ = ๐‘)))
208175, 140, 178, 207syl3anc 1372 . . . . 5 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ ((๐ท โˆˆ On โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐‘‹) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” (๐ท = ๐‘Œ โˆง ๐ธ = ๐‘)))
209174, 208sylan9bbr 512 . . . 4 (((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โˆง ๐ถ = ๐‘‹) โ†’ ((๐ท โˆˆ On โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ†” (๐ท = ๐‘Œ โˆง ๐ธ = ๐‘)))
210209pm5.32da 580 . . 3 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ ((๐ถ = ๐‘‹ โˆง (๐ท โˆˆ On โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต))) โ†” (๐ถ = ๐‘‹ โˆง (๐ท = ๐‘Œ โˆง ๐ธ = ๐‘))))
211166, 210bitrd 279 . 2 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ†” (๐ถ = ๐‘‹ โˆง (๐ท = ๐‘Œ โˆง ๐ธ = ๐‘))))
212 3an4anass 1106 . 2 (((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o) โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐ถ)) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” ((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o)) โˆง (๐ธ โˆˆ (๐ด โ†‘o ๐ถ) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)))
213 3anass 1096 . 2 ((๐ถ = ๐‘‹ โˆง ๐ท = ๐‘Œ โˆง ๐ธ = ๐‘) โ†” (๐ถ = ๐‘‹ โˆง (๐ท = ๐‘Œ โˆง ๐ธ = ๐‘)))
214211, 212, 2133bitr4g 314 1 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ต โˆˆ (On โˆ– 1o)) โ†’ (((๐ถ โˆˆ On โˆง ๐ท โˆˆ (๐ด โˆ– 1o) โˆง ๐ธ โˆˆ (๐ด โ†‘o ๐ถ)) โˆง (((๐ด โ†‘o ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ†” (๐ถ = ๐‘‹ โˆง ๐ท = ๐‘Œ โˆง ๐ธ = ๐‘)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆƒ!weu 2567   โ‰  wne 2944  โˆƒwrex 3074  {crab 3410   โˆ– cdif 3912   โŠ† wss 3915  โˆ…c0 4287  {csn 4591  โŸจcop 4597  โˆช cuni 4870  โˆฉ cint 4912  Ord word 6321  Oncon0 6322  suc csuc 6324  โ„ฉcio 6451  โ€˜cfv 6501  (class class class)co 7362  1st c1st 7924  2nd c2nd 7925  1oc1o 8410  2oc2o 8411   +o coa 8414   ยทo comu 8415   โ†‘o coe 8416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-oexp 8423
This theorem is referenced by:  oeeu  8555  cantnflem3  9634  cantnflem4  9635
  Copyright terms: Public domain W3C validator