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

Theorem omabs2 42639
Description: Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or ฯ‰ raised to some power of ฯ‰. (Contributed by RP, 12-Jan-2025.)
Assertion
Ref Expression
omabs2 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = โˆ… โˆจ ๐ต = 2o โˆจ (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On))) โ†’ (๐ด ยทo ๐ต) = ๐ต)

Proof of Theorem omabs2
Dummy variables ๐‘ค ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2816 . . . . . 6 (๐ต = โˆ… โ†’ (๐ด โˆˆ ๐ต โ†” ๐ด โˆˆ โˆ…))
2 noel 4325 . . . . . . 7 ยฌ ๐ด โˆˆ โˆ…
32pm2.21i 119 . . . . . 6 (๐ด โˆˆ โˆ… โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) = ๐ต))
41, 3syl6bi 253 . . . . 5 (๐ต = โˆ… โ†’ (๐ด โˆˆ ๐ต โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) = ๐ต)))
54impd 410 . . . 4 (๐ต = โˆ… โ†’ ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
65com12 32 . . 3 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ต = โˆ… โ†’ (๐ด ยทo ๐ต) = ๐ต))
7 elpri 4645 . . . . . . . . 9 (๐ด โˆˆ {โˆ…, 1o} โ†’ (๐ด = โˆ… โˆจ ๐ด = 1o))
8 eleq2 2816 . . . . . . . . . . 11 (๐ด = โˆ… โ†’ (โˆ… โˆˆ ๐ด โ†” โˆ… โˆˆ โˆ…))
9 noel 4325 . . . . . . . . . . . 12 ยฌ โˆ… โˆˆ โˆ…
109pm2.21i 119 . . . . . . . . . . 11 (โˆ… โˆˆ โˆ… โ†’ (๐ด ยทo 2o) = 2o)
118, 10syl6bi 253 . . . . . . . . . 10 (๐ด = โˆ… โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
12 oveq1 7411 . . . . . . . . . . . 12 (๐ด = 1o โ†’ (๐ด ยทo 2o) = (1o ยทo 2o))
13 2on 8478 . . . . . . . . . . . . 13 2o โˆˆ On
14 om1r 8541 . . . . . . . . . . . . 13 (2o โˆˆ On โ†’ (1o ยทo 2o) = 2o)
1513, 14ax-mp 5 . . . . . . . . . . . 12 (1o ยทo 2o) = 2o
1612, 15eqtrdi 2782 . . . . . . . . . . 11 (๐ด = 1o โ†’ (๐ด ยทo 2o) = 2o)
1716a1d 25 . . . . . . . . . 10 (๐ด = 1o โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
1811, 17jaoi 854 . . . . . . . . 9 ((๐ด = โˆ… โˆจ ๐ด = 1o) โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
197, 18syl 17 . . . . . . . 8 (๐ด โˆˆ {โˆ…, 1o} โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
20 df2o3 8472 . . . . . . . 8 2o = {โˆ…, 1o}
2119, 20eleq2s 2845 . . . . . . 7 (๐ด โˆˆ 2o โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
2221imp 406 . . . . . 6 ((๐ด โˆˆ 2o โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo 2o) = 2o)
2322a1i 11 . . . . 5 (๐ต = 2o โ†’ ((๐ด โˆˆ 2o โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo 2o) = 2o))
24 eleq2 2816 . . . . . 6 (๐ต = 2o โ†’ (๐ด โˆˆ ๐ต โ†” ๐ด โˆˆ 2o))
2524anbi1d 629 . . . . 5 (๐ต = 2o โ†’ ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†” (๐ด โˆˆ 2o โˆง โˆ… โˆˆ ๐ด)))
26 oveq2 7412 . . . . . 6 (๐ต = 2o โ†’ (๐ด ยทo ๐ต) = (๐ด ยทo 2o))
27 id 22 . . . . . 6 (๐ต = 2o โ†’ ๐ต = 2o)
2826, 27eqeq12d 2742 . . . . 5 (๐ต = 2o โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo 2o) = 2o))
2923, 25, 283imtr4d 294 . . . 4 (๐ต = 2o โ†’ ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
3029com12 32 . . 3 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ต = 2o โ†’ (๐ด ยทo ๐ต) = ๐ต))
31 simpr 484 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ ๐ด โˆˆ ฯ‰)
32 simpllr 773 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ โˆ… โˆˆ ๐ด)
33 omelon 9640 . . . . . . . . . 10 ฯ‰ โˆˆ On
34 oecl 8535 . . . . . . . . . 10 ((ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3533, 34mpan 687 . . . . . . . . 9 (๐ถ โˆˆ On โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3635adantl 481 . . . . . . . 8 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3736ad2antlr 724 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3833jctl 523 . . . . . . . . . 10 (๐ถ โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On))
39 peano1 7875 . . . . . . . . . 10 โˆ… โˆˆ ฯ‰
40 oen0 8584 . . . . . . . . . 10 (((ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
4138, 39, 40sylancl 585 . . . . . . . . 9 (๐ถ โˆˆ On โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
4241adantl 481 . . . . . . . 8 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
4342ad2antlr 724 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
44 omabs 8649 . . . . . . 7 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
4531, 32, 37, 43, 44syl22anc 836 . . . . . 6 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
46 oveq2 7412 . . . . . . . . 9 (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐ด ยทo ๐ต) = (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
47 id 22 . . . . . . . . 9 (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
4846, 47eqeq12d 2742 . . . . . . . 8 (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
4948adantr 480 . . . . . . 7 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
5049ad2antlr 724 . . . . . 6 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
5145, 50mpbird 257 . . . . 5 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ (๐ด ยทo ๐ต) = ๐ต)
52 simpl 482 . . . . . . . . . . . 12 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
53 oecl 8535 . . . . . . . . . . . . . 14 ((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
5433, 35, 53sylancr 586 . . . . . . . . . . . . 13 (๐ถ โˆˆ On โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
5554adantl 481 . . . . . . . . . . . 12 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
5652, 55eqeltrd 2827 . . . . . . . . . . 11 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ ๐ต โˆˆ On)
57 simpl 482 . . . . . . . . . . 11 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ ๐ด โˆˆ ๐ต)
58 onelon 6382 . . . . . . . . . . 11 ((๐ต โˆˆ On โˆง ๐ด โˆˆ ๐ต) โ†’ ๐ด โˆˆ On)
5956, 57, 58syl2anr 596 . . . . . . . . . 10 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ๐ด โˆˆ On)
60 simplr 766 . . . . . . . . . 10 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ โˆ… โˆˆ ๐ด)
61 ondif1 8499 . . . . . . . . . 10 (๐ด โˆˆ (On โˆ– 1o) โ†” (๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด))
6259, 60, 61sylanbrc 582 . . . . . . . . 9 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ๐ด โˆˆ (On โˆ– 1o))
63 1onn 8638 . . . . . . . . . 10 1o โˆˆ ฯ‰
64 ondif2 8500 . . . . . . . . . 10 (ฯ‰ โˆˆ (On โˆ– 2o) โ†” (ฯ‰ โˆˆ On โˆง 1o โˆˆ ฯ‰))
6533, 63, 64mpbir2an 708 . . . . . . . . 9 ฯ‰ โˆˆ (On โˆ– 2o)
6662, 65jctil 519 . . . . . . . 8 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (ฯ‰ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ (On โˆ– 1o)))
6766adantr 480 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โ†’ (ฯ‰ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ (On โˆ– 1o)))
68 oeeu 8601 . . . . . . 7 ((ฯ‰ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ (On โˆ– 1o)) โ†’ โˆƒ!๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด))
6967, 68syl 17 . . . . . 6 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โ†’ โˆƒ!๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด))
70 euex 2565 . . . . . . 7 (โˆƒ!๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ โˆƒ๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด))
71 simpr 484 . . . . . . . . . . . 12 ((๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด)
72 0ss 4391 . . . . . . . . . . . . . . . . . . 19 โˆ… โІ ๐‘ง
73 0elon 6411 . . . . . . . . . . . . . . . . . . . 20 โˆ… โˆˆ On
74 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ On)
75 oecl 8535 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
7633, 74, 75sylancr 586 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
7776ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
78 onelon 6382 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
7977, 78sylancom 587 . . . . . . . . . . . . . . . . . . . 20 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
80 1on 8476 . . . . . . . . . . . . . . . . . . . . . 22 1o โˆˆ On
81 omcl 8534 . . . . . . . . . . . . . . . . . . . . . 22 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง 1o โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
8276, 80, 81sylancl 585 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
8382ad5ant12 753 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
84 oaword 8547 . . . . . . . . . . . . . . . . . . . . 21 ((โˆ… โˆˆ On โˆง ๐‘ง โˆˆ On โˆง ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On) โ†’ (โˆ… โІ ๐‘ง โ†” (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o ๐‘ง)))
8584biimpd 228 . . . . . . . . . . . . . . . . . . . 20 ((โˆ… โˆˆ On โˆง ๐‘ง โˆˆ On โˆง ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On) โ†’ (โˆ… โІ ๐‘ง โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o ๐‘ง)))
8673, 79, 83, 85mp3an2ani 1464 . . . . . . . . . . . . . . . . . . 19 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (โˆ… โІ ๐‘ง โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o ๐‘ง)))
8772, 86mpi 20 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o ๐‘ง))
88 simpllr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o))
89 omsson 7855 . . . . . . . . . . . . . . . . . . . . . . 23 ฯ‰ โІ On
90 ssdif 4134 . . . . . . . . . . . . . . . . . . . . . . 23 (ฯ‰ โІ On โ†’ (ฯ‰ โˆ– 1o) โІ (On โˆ– 1o))
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (ฯ‰ โˆ– 1o) โІ (On โˆ– 1o)
9291sseli 3973 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o) โ†’ ๐‘ฆ โˆˆ (On โˆ– 1o))
93 ondif1 8499 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ (On โˆ– 1o) โ†” (๐‘ฆ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฆ))
94 df-1o 8464 . . . . . . . . . . . . . . . . . . . . . . 23 1o = suc โˆ…
95 eloni 6367 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ On โ†’ Ord ๐‘ฆ)
96 ordsucss 7802 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord ๐‘ฆ โ†’ (โˆ… โˆˆ ๐‘ฆ โ†’ suc โˆ… โІ ๐‘ฆ))
9795, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฆ โ†’ suc โˆ… โІ ๐‘ฆ))
9897imp 406 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฆ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฆ) โ†’ suc โˆ… โІ ๐‘ฆ)
9994, 98eqsstrid 4025 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฆ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฆ) โ†’ 1o โІ ๐‘ฆ)
10093, 99sylbi 216 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ (On โˆ– 1o) โ†’ 1o โІ ๐‘ฆ)
10188, 92, 1003syl 18 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ 1o โІ ๐‘ฆ)
102 eldifi 4121 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o) โ†’ ๐‘ฆ โˆˆ ฯ‰)
103 nnon 7857 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ ฯ‰ โ†’ ๐‘ฆ โˆˆ On)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o) โ†’ ๐‘ฆ โˆˆ On)
105104ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ฆ โˆˆ On)
106 simp-4r 781 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฅ โˆˆ On)
10733, 106, 75sylancr 586 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
108 omwordi 8569 . . . . . . . . . . . . . . . . . . . . 21 ((1o โˆˆ On โˆง ๐‘ฆ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (1o โІ ๐‘ฆ โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ)))
10980, 105, 107, 108mp3an2ani 1464 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (1o โІ ๐‘ฆ โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ)))
110101, 109mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ))
111105adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฆ โˆˆ On)
112 omcl 8534 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On)
113107, 111, 112syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On)
11479adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ง โˆˆ On)
115 oawordri 8548 . . . . . . . . . . . . . . . . . . . 20 ((((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On โˆง ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On โˆง ๐‘ง โˆˆ On) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o ๐‘ง) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง)))
11683, 113, 114, 115syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o ๐‘ง) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง)))
117110, 116mpd 15 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o ๐‘ง) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง))
11887, 117sstrd 3987 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง))
11933, 75mpan 687 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ On โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
120119, 80, 81sylancl 585 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ On โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
121 oa0 8514 . . . . . . . . . . . . . . . . . . . 20 (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o))
122120, 121syl 17 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ On โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o))
123 om1 8540 . . . . . . . . . . . . . . . . . . . 20 ((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) = (ฯ‰ โ†‘o ๐‘ฅ))
124119, 123syl 17 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ On โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) = (ฯ‰ โ†‘o ๐‘ฅ))
125122, 124eqtrd 2766 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ On โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) = (ฯ‰ โ†‘o ๐‘ฅ))
126106, 125syl 17 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) = (ฯ‰ โ†‘o ๐‘ฅ))
127 simpr 484 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด)
128118, 126, 1273sstr3d 4023 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โІ ๐ด)
129 simp-7l 786 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด โˆˆ ๐ต)
130 simplrl 774 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
131130ad4antr 729 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
132129, 131eleqtrd 2829 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
13355ad6antlr 734 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
134 ontr2 6404 . . . . . . . . . . . . . . . . 17 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) โІ ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
135107, 133, 134syl2anc 583 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) โІ ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
136128, 132, 135mp2and 696 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
13736ad6antlr 734 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
13865a1i 11 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
139 oeord 8586 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
140106, 137, 138, 139syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
141136, 140mpbird 257 . . . . . . . . . . . . . 14 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ))
142 simp-5r 783 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ฯ‰ โІ ๐ด)
143142, 128unssd 4181 . . . . . . . . . . . . . 14 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด)
144 simplr 766 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
145 onelpss 6397 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ง โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†” (๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ))))
146145biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ง โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ))))
14779, 107, 146syl2an2r 682 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ))))
148144, 147mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ)))
149 simpl 482 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ))
150148, 149syl 17 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ))
151 oaword 8547 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ง โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On) โ†’ (๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โ†” (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ))))
152151biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On) โ†’ (๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ))))
153114, 107, 113, 152syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ง โІ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ))))
154150, 153mpd 15 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โІ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ)))
155 omsuc 8524 . . . . . . . . . . . . . . . . . 18 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ)))
156107, 111, 155syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ)))
157154, 156sseqtrrd 4018 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ))
158 ordom 7861 . . . . . . . . . . . . . . . . . . 19 Ord ฯ‰
15988, 102syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฆ โˆˆ ฯ‰)
160 ordsucss 7802 . . . . . . . . . . . . . . . . . . 19 (Ord ฯ‰ โ†’ (๐‘ฆ โˆˆ ฯ‰ โ†’ suc ๐‘ฆ โІ ฯ‰))
161158, 159, 160mpsyl 68 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ suc ๐‘ฆ โІ ฯ‰)
162 oe1 8542 . . . . . . . . . . . . . . . . . . . 20 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o 1o) = ฯ‰)
16333, 162ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (ฯ‰ โ†‘o 1o) = ฯ‰
164 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฅ = โˆ…)
165164oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o โˆ…))
166 oe0 8520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o โˆ…) = 1o)
16733, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ฯ‰ โ†‘o โˆ…) = 1o
168165, 167eqtrdi 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = 1o)
169168oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) = (1o ยทo ๐‘ฆ))
170104adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โ†’ ๐‘ฆ โˆˆ On)
171170ad5ant12 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฆ โˆˆ On)
172 om1r 8541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฆ โˆˆ On โ†’ (1o ยทo ๐‘ฆ) = ๐‘ฆ)
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (1o ยทo ๐‘ฆ) = ๐‘ฆ)
174169, 173eqtrd 2766 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) = ๐‘ฆ)
175 simpllr 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
176175, 168eleqtrd 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ง โˆˆ 1o)
177 el1o 8493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ง โˆˆ 1o โ†” ๐‘ง = โˆ…)
178176, 177sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ง = โˆ…)
179174, 178oveq12d 7422 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = (๐‘ฆ +o โˆ…))
180 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด)
181 oa0 8514 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ On โ†’ (๐‘ฆ +o โˆ…) = ๐‘ฆ)
182171, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฆ +o โˆ…) = ๐‘ฆ)
183179, 180, 1823eqtr3d 2774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐ด = ๐‘ฆ)
184159adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฆ โˆˆ ฯ‰)
185183, 184eqeltrd 2827 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐ด โˆˆ ฯ‰)
186185ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ฅ = โˆ… โ†’ ๐ด โˆˆ ฯ‰))
18733, 33pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . 23 (ฯ‰ โˆˆ On โˆง ฯ‰ โˆˆ On)
188 ontr2 6404 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ฯ‰ โˆˆ On โˆง ฯ‰ โˆˆ On) โ†’ ((ฯ‰ โІ ๐ด โˆง ๐ด โˆˆ ฯ‰) โ†’ ฯ‰ โˆˆ ฯ‰))
189188expd 415 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โˆˆ On โˆง ฯ‰ โˆˆ On) โ†’ (ฯ‰ โІ ๐ด โ†’ (๐ด โˆˆ ฯ‰ โ†’ ฯ‰ โˆˆ ฯ‰)))
190187, 142, 189mpsyl 68 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด โˆˆ ฯ‰ โ†’ ฯ‰ โˆˆ ฯ‰))
191 elirr 9591 . . . . . . . . . . . . . . . . . . . . . . . 24 ยฌ ฯ‰ โˆˆ ฯ‰
192191pm2.21i 119 . . . . . . . . . . . . . . . . . . . . . . 23 (ฯ‰ โˆˆ ฯ‰ โ†’ 1o โІ ๐‘ฅ)
193192a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โˆˆ ฯ‰ โ†’ 1o โІ ๐‘ฅ))
194186, 190, 1933syld 60 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ฅ = โˆ… โ†’ 1o โІ ๐‘ฅ))
195 eloni 6367 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ On โ†’ Ord ๐‘ฅ)
196 ordsucss 7802 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord ๐‘ฅ โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ suc โˆ… โІ ๐‘ฅ))
197196imp 406 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Ord ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ suc โˆ… โІ ๐‘ฅ)
19894, 197eqsstrid 4025 . . . . . . . . . . . . . . . . . . . . . . 23 ((Ord ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ 1o โІ ๐‘ฅ)
199198ex 412 . . . . . . . . . . . . . . . . . . . . . 22 (Ord ๐‘ฅ โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ 1o โІ ๐‘ฅ))
200106, 195, 1993syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ 1o โІ ๐‘ฅ))
201 on0eqel 6481 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
202106, 201syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
203194, 200, 202mpjaod 857 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ 1o โІ ๐‘ฅ)
20480a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ 1o โˆˆ On)
20533a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ฯ‰ โˆˆ On)
206204, 106, 2053jca 1125 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (1o โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ฯ‰ โˆˆ On))
207 oewordi 8589 . . . . . . . . . . . . . . . . . . . . 21 (((1o โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ฯ‰ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ (1o โІ ๐‘ฅ โ†’ (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐‘ฅ)))
208206, 39, 207sylancl 585 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (1o โІ ๐‘ฅ โ†’ (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐‘ฅ)))
209203, 208mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐‘ฅ))
210163, 209eqsstrrid 4026 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ฯ‰ โІ (ฯ‰ โ†‘o ๐‘ฅ))
211161, 210sstrd 3987 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ suc ๐‘ฆ โІ (ฯ‰ โ†‘o ๐‘ฅ))
212 onsuc 7795 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ โˆˆ On โ†’ suc ๐‘ฆ โˆˆ On)
213111, 212syl 17 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ suc ๐‘ฆ โˆˆ On)
214 omwordi 8569 . . . . . . . . . . . . . . . . . 18 ((suc ๐‘ฆ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (suc ๐‘ฆ โІ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ))))
215213, 107, 107, 214syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (suc ๐‘ฆ โІ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ))))
216211, 215mpd 15 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
217157, 216sstrd 3987 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โІ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
218127eqcomd 2732 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง))
219 oeoa 8595 . . . . . . . . . . . . . . . 16 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
22033, 106, 106, 219mp3an2i 1462 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
221217, 218, 2203sstr4d 4024 . . . . . . . . . . . . . 14 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))
222 simpr3 1193 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))
22359adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โˆˆ On)
224 simprr 770 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ๐ถ โˆˆ On)
225 simp1 1133 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ))
226224, 225anim12i 612 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)))
227 onelon 6382 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ ๐‘ฅ โˆˆ On)
22835, 227sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ ๐‘ฅ โˆˆ On)
229 pm4.24 563 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ On โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On))
230228, 229sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On))
231 oacl 8533 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฅ +o ๐‘ฅ) โˆˆ On)
232230, 231syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐‘ฅ +o ๐‘ฅ) โˆˆ On)
233 oecl 8535 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โˆˆ On โˆง (๐‘ฅ +o ๐‘ฅ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On)
23433, 232, 233sylancr 586 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On)
235226, 234syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On)
23655ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
237 omwordri 8570 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด โˆˆ On โˆง (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On) โ†’ (๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โІ ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))))
238223, 235, 236, 237syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โІ ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))))
239222, 238mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โІ ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
240226, 230, 2313syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐‘ฅ +o ๐‘ฅ) โˆˆ On)
24136ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
242 oeoa 8595 . . . . . . . . . . . . . . . . . . . . 21 ((ฯ‰ โˆˆ On โˆง (๐‘ฅ +o ๐‘ฅ) โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (ฯ‰ โ†‘o ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
24333, 240, 241, 242mp3an2i 1462 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
244226, 228syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐‘ฅ โˆˆ On)
245 oaass 8559 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ)) = (๐‘ฅ +o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))))
246244, 244, 241, 245syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ)) = (๐‘ฅ +o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))))
247 simpr1 1191 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ))
248 ssidd 4000 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o ๐ถ) โІ (ฯ‰ โ†‘o ๐ถ))
249 oaabs2 8647 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โІ (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
250247, 241, 248, 249syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
251250oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐‘ฅ +o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)))
252246, 251, 2503eqtrd 2770 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
253252oveq2d 7420 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
254243, 253eqtr3d 2768 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
255239, 254sseqtrd 4017 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โІ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
256 oveq2 7412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o โˆ…))
257256, 167eqtrdi 2782 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = 1o)
258257uneq2d 4158 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โˆช 1o))
25933oneluni 6476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1o โˆˆ ฯ‰ โ†’ (ฯ‰ โˆช 1o) = ฯ‰)
26063, 259ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ฯ‰ โˆช 1o) = ฯ‰
261260, 163eqtr4i 2757 . . . . . . . . . . . . . . . . . . . . . . . 24 (ฯ‰ โˆช 1o) = (ฯ‰ โ†‘o 1o)
262258, 261eqtrdi 2782 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o 1o))
263262adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o 1o))
264263oveq1d 7419 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o 1o) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
265224ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ๐ถ โˆˆ On)
266 oecl 8535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((ฯ‰ โˆˆ On โˆง โˆ… โˆˆ On) โ†’ (ฯ‰ โ†‘o โˆ…) โˆˆ On)
26733, 73, 266mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ฯ‰ โ†‘o โˆ…) โˆˆ On
268 oecl 8535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o โˆ…) โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On)
26933, 267, 268mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On
2702692a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On))
271270, 54jca2 513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)))
272167oveq2i 7415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) = (ฯ‰ โ†‘o 1o)
273272, 163eqtri 2754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) = ฯ‰
274 ssun1 4167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ฯ‰ โІ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ))
275273, 274eqsstri 4011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โІ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ))
276 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด)
277275, 276sstrid 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โІ ๐ด)
278277adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โІ ๐ด)
27957ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โˆˆ ๐ต)
280 simplrl 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
281279, 280eleqtrd 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
282278, 281jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โІ ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
283282adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โІ ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
284 ontr2 6404 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On) โ†’ (((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โІ ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
285271, 283, 284syl6ci 71 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
286 oeord 8586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((โˆ… โˆˆ On โˆง ๐ถ โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (โˆ… โˆˆ ๐ถ โ†” (ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ)))
28773, 65, 286mp3an13 1448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†” (ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ)))
28865a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐ถ โˆˆ On โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
289 oeord 8586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ฯ‰ โ†‘o โˆ…) โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ ((ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
290267, 35, 288, 289mp3an2i 1462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐ถ โˆˆ On โ†’ ((ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
291287, 290bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†” (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
292291biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ถ โˆˆ On โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ โˆ… โˆˆ ๐ถ))
293285, 292sylcom 30 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ โˆ… โˆˆ ๐ถ))
294 eloni 6367 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ถ โˆˆ On โ†’ Ord ๐ถ)
295 ordsucss 7802 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord ๐ถ โ†’ (โˆ… โˆˆ ๐ถ โ†’ suc โˆ… โІ ๐ถ))
29694sseq1i 4005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1o โІ ๐ถ โ†” suc โˆ… โІ ๐ถ)
297295, 296imbitrrdi 251 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord ๐ถ โ†’ (โˆ… โˆˆ ๐ถ โ†’ 1o โІ ๐ถ))
298294, 297syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†’ 1o โІ ๐ถ))
299293, 298sylcom 30 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ 1o โІ ๐ถ))
300265, 299jcai 516 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โˆง 1o โІ ๐ถ))
30133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ถ โˆˆ On โ†’ ฯ‰ โˆˆ On)
30280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ถ โˆˆ On โ†’ 1o โˆˆ On)
303301, 302, 353jca 1125 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ถ โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง 1o โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On))
304303adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ (ฯ‰ โˆˆ On โˆง 1o โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On))
305 oeoa 8595 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ฯ‰ โˆˆ On โˆง 1o โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (1o +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o 1o) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
306304, 305syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ (ฯ‰ โ†‘o (1o +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o 1o) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
30763a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ 1o โˆˆ ฯ‰)
30835adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
309 oeword 8588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1o โˆˆ On โˆง ๐ถ โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (1o โІ ๐ถ โ†” (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐ถ)))
31080, 65, 309mp3an13 1448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐ถ โˆˆ On โ†’ (1o โІ ๐ถ โ†” (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐ถ)))
311310biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐ถ))
312163, 311eqsstrrid 4026 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ ฯ‰ โІ (ฯ‰ โ†‘o ๐ถ))
313 oaabs 8646 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1o โˆˆ ฯ‰ โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โˆง ฯ‰ โІ (ฯ‰ โ†‘o ๐ถ)) โ†’ (1o +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
314307, 308, 312, 313syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ (1o +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
315314oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ (ฯ‰ โ†‘o (1o +o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
316306, 315eqtr3d 2768 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ถ โˆˆ On โˆง 1o โІ ๐ถ) โ†’ ((ฯ‰ โ†‘o 1o) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
317300, 316syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โ†‘o 1o) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
318264, 317eqtrd 2766 . . . . . . . . . . . . . . . . . . . 20 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
319244, 195, 1963syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ suc โˆ… โІ ๐‘ฅ))
320319imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ suc โˆ… โІ ๐‘ฅ)
32194, 320eqsstrid 4025 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ 1o โІ ๐‘ฅ)
322247adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ))
323241, 322, 227syl2an2r 682 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ On)
32465a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
325 oeword 8588 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1o โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (1o โІ ๐‘ฅ โ†” (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐‘ฅ)))
32680, 323, 324, 325mp3an2i 1462 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (1o โІ ๐‘ฅ โ†” (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐‘ฅ)))
327321, 326mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o 1o) โІ (ฯ‰ โ†‘o ๐‘ฅ))
328163, 327eqsstrrid 4026 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ฯ‰ โІ (ฯ‰ โ†‘o ๐‘ฅ))
329 ssequn1 4175 . . . . . . . . . . . . . . . . . . . . . . 23 (ฯ‰ โІ (ฯ‰ โ†‘o ๐‘ฅ) โ†” (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ))
330328, 329sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ))
331330oveq1d 7419 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
332241adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
333 oeoa 8595 . . . . . . . . . . . . . . . . . . . . . 22 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
33433, 323, 332, 333mp3an2i 1462 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
335 ssidd 4000 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o ๐ถ) โІ (ฯ‰ โ†‘o ๐ถ))
336322, 332, 335, 249syl21anc 835 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
337336oveq2d 7420 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
338331, 334, 3373eqtr2d 2772 . . . . . . . . . . . . . . . . . . . 20 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
339226, 228, 2013syl 18 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
340318, 338, 339mpjaodan 955 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
341276adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด)
34233, 228, 75sylancr 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
343342, 33jctil 519 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On))
344 onun2 6465 . . . . . . . . . . . . . . . . . . . . . 22 ((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โˆˆ On)
345226, 343, 3443syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โˆˆ On)
346 omwordri 8570 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โˆˆ On โˆง ๐ด โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โІ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))))
347345, 223, 236, 346syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โІ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))))
348341, 347mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โІ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
349340, 348eqsstrrd 4016 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โІ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
350255, 349eqssd 3994 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
35149ad2antlr 724 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
352350, 351mpbird 257 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ด ยทo ๐ต) = ๐ต)
353352ex 412 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (๐ด ยทo ๐ต) = ๐ต))
354353ad5antr 731 . . . . . . . . . . . . . 14 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โІ ๐ด โˆง ๐ด โІ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (๐ด ยทo ๐ต) = ๐ต))
355141, 143, 221, 354mp3and 1460 . . . . . . . . . . . . 13 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต)
356355ex 412 . . . . . . . . . . . 12 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ((((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด โ†’ (๐ด ยทo ๐ต) = ๐ต))
35771, 356syl5 34 . . . . . . . . . . 11 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ((๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
358357rexlimdva 3149 . . . . . . . . . 10 ((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โ†’ (โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
359358rexlimdva 3149 . . . . . . . . 9 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
360359rexlimdva 3149 . . . . . . . 8 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โ†’ (โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
361360exlimdv 1928 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
36270, 361syl5 34 . . . . . 6 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โ†’ (โˆƒ!๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
36369, 362mpd 15 . . . . 5 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โІ ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต)
364 eloni 6367 . . . . . . 7 (๐ด โˆˆ On โ†’ Ord ๐ด)
36559, 364syl 17 . . . . . 6 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ Ord ๐ด)
366 ordtri2or 6455 . . . . . 6 ((Ord ๐ด โˆง Ord ฯ‰) โ†’ (๐ด โˆˆ ฯ‰ โˆจ ฯ‰ โІ ๐ด))
367365, 158, 366sylancl 585 . . . . 5 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (๐ด โˆˆ ฯ‰ โˆจ ฯ‰ โІ ๐ด))
36851, 363, 367mpjaodan 955 . . . 4 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (๐ด ยทo ๐ต) = ๐ต)
369368ex 412 . . 3 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ (๐ด ยทo ๐ต) = ๐ต))
3706, 30, 3693jaod 1425 . 2 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ต = โˆ… โˆจ ๐ต = 2o โˆจ (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (๐ด ยทo ๐ต) = ๐ต))
371370imp 406 1 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = โˆ… โˆจ ๐ต = 2o โˆจ (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On))) โ†’ (๐ด ยทo ๐ต) = ๐ต)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆจ w3o 1083   โˆง w3a 1084   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098  โˆƒ!weu 2556   โ‰  wne 2934  โˆƒwrex 3064   โˆ– cdif 3940   โˆช cun 3941   โІ wss 3943  โˆ…c0 4317  {cpr 4625  โŸจcotp 4631  Ord word 6356  Oncon0 6357  suc csuc 6359  (class class class)co 7404  ฯ‰com 7851  1oc1o 8457  2oc2o 8458   +o coa 8461   ยทo comu 8462   โ†‘o coe 8463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7721  ax-reg 9586  ax-inf2 9635
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-ot 4632  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-2o 8465  df-oadd 8468  df-omul 8469  df-oexp 8470
This theorem is referenced by:  omcl2  42640
  Copyright terms: Public domain W3C validator