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 41710
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 2823 . . . . . 6 (๐ต = โˆ… โ†’ (๐ด โˆˆ ๐ต โ†” ๐ด โˆˆ โˆ…))
2 noel 4291 . . . . . . 7 ยฌ ๐ด โˆˆ โˆ…
32pm2.21i 119 . . . . . 6 (๐ด โˆˆ โˆ… โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) = ๐ต))
41, 3syl6bi 253 . . . . 5 (๐ต = โˆ… โ†’ (๐ด โˆˆ ๐ต โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) = ๐ต)))
54impd 412 . . . 4 (๐ต = โˆ… โ†’ ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
65com12 32 . . 3 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ต = โˆ… โ†’ (๐ด ยทo ๐ต) = ๐ต))
7 elpri 4609 . . . . . . . . 9 (๐ด โˆˆ {โˆ…, 1o} โ†’ (๐ด = โˆ… โˆจ ๐ด = 1o))
8 eleq2 2823 . . . . . . . . . . 11 (๐ด = โˆ… โ†’ (โˆ… โˆˆ ๐ด โ†” โˆ… โˆˆ โˆ…))
9 noel 4291 . . . . . . . . . . . 12 ยฌ โˆ… โˆˆ โˆ…
109pm2.21i 119 . . . . . . . . . . 11 (โˆ… โˆˆ โˆ… โ†’ (๐ด ยทo 2o) = 2o)
118, 10syl6bi 253 . . . . . . . . . 10 (๐ด = โˆ… โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
12 oveq1 7365 . . . . . . . . . . . 12 (๐ด = 1o โ†’ (๐ด ยทo 2o) = (1o ยทo 2o))
13 2on 8427 . . . . . . . . . . . . 13 2o โˆˆ On
14 om1r 8491 . . . . . . . . . . . . 13 (2o โˆˆ On โ†’ (1o ยทo 2o) = 2o)
1513, 14ax-mp 5 . . . . . . . . . . . 12 (1o ยทo 2o) = 2o
1612, 15eqtrdi 2789 . . . . . . . . . . 11 (๐ด = 1o โ†’ (๐ด ยทo 2o) = 2o)
1716a1d 25 . . . . . . . . . 10 (๐ด = 1o โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
1811, 17jaoi 856 . . . . . . . . 9 ((๐ด = โˆ… โˆจ ๐ด = 1o) โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
197, 18syl 17 . . . . . . . 8 (๐ด โˆˆ {โˆ…, 1o} โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
20 df2o3 8421 . . . . . . . 8 2o = {โˆ…, 1o}
2119, 20eleq2s 2852 . . . . . . 7 (๐ด โˆˆ 2o โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo 2o) = 2o))
2221imp 408 . . . . . 6 ((๐ด โˆˆ 2o โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo 2o) = 2o)
2322a1i 11 . . . . 5 (๐ต = 2o โ†’ ((๐ด โˆˆ 2o โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo 2o) = 2o))
24 eleq2 2823 . . . . . 6 (๐ต = 2o โ†’ (๐ด โˆˆ ๐ต โ†” ๐ด โˆˆ 2o))
2524anbi1d 631 . . . . 5 (๐ต = 2o โ†’ ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†” (๐ด โˆˆ 2o โˆง โˆ… โˆˆ ๐ด)))
26 oveq2 7366 . . . . . 6 (๐ต = 2o โ†’ (๐ด ยทo ๐ต) = (๐ด ยทo 2o))
27 id 22 . . . . . 6 (๐ต = 2o โ†’ ๐ต = 2o)
2826, 27eqeq12d 2749 . . . . 5 (๐ต = 2o โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo 2o) = 2o))
2923, 25, 283imtr4d 294 . . . 4 (๐ต = 2o โ†’ ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต))
3029com12 32 . . 3 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ต = 2o โ†’ (๐ด ยทo ๐ต) = ๐ต))
31 simpr 486 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ ๐ด โˆˆ ฯ‰)
32 simpllr 775 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ โˆ… โˆˆ ๐ด)
33 omelon 9587 . . . . . . . . . 10 ฯ‰ โˆˆ On
34 oecl 8484 . . . . . . . . . 10 ((ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3533, 34mpan 689 . . . . . . . . 9 (๐ถ โˆˆ On โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3635adantl 483 . . . . . . . 8 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3736ad2antlr 726 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
3833jctl 525 . . . . . . . . . 10 (๐ถ โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On))
39 peano1 7826 . . . . . . . . . 10 โˆ… โˆˆ ฯ‰
40 oen0 8534 . . . . . . . . . 10 (((ฯ‰ โˆˆ On โˆง ๐ถ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
4138, 39, 40sylancl 587 . . . . . . . . 9 (๐ถ โˆˆ On โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
4241adantl 483 . . . . . . . 8 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
4342ad2antlr 726 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))
44 omabs 8598 . . . . . . 7 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง โˆ… โˆˆ (ฯ‰ โ†‘o ๐ถ))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
4531, 32, 37, 43, 44syl22anc 838 . . . . . 6 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
46 oveq2 7366 . . . . . . . . 9 (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐ด ยทo ๐ต) = (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
47 id 22 . . . . . . . . 9 (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
4846, 47eqeq12d 2749 . . . . . . . 8 (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
4948adantr 482 . . . . . . 7 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
5049ad2antlr 726 . . . . . 6 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ ((๐ด ยทo ๐ต) = ๐ต โ†” (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
5145, 50mpbird 257 . . . . 5 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ๐ด โˆˆ ฯ‰) โ†’ (๐ด ยทo ๐ต) = ๐ต)
52 simpl 484 . . . . . . . . . . . 12 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
53 oecl 8484 . . . . . . . . . . . . . 14 ((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
5433, 35, 53sylancr 588 . . . . . . . . . . . . 13 (๐ถ โˆˆ On โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
5554adantl 483 . . . . . . . . . . . 12 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
5652, 55eqeltrd 2834 . . . . . . . . . . 11 ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ ๐ต โˆˆ On)
57 simpl 484 . . . . . . . . . . 11 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ ๐ด โˆˆ ๐ต)
58 onelon 6343 . . . . . . . . . . 11 ((๐ต โˆˆ On โˆง ๐ด โˆˆ ๐ต) โ†’ ๐ด โˆˆ On)
5956, 57, 58syl2anr 598 . . . . . . . . . 10 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ๐ด โˆˆ On)
60 simplr 768 . . . . . . . . . 10 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ โˆ… โˆˆ ๐ด)
61 ondif1 8448 . . . . . . . . . 10 (๐ด โˆˆ (On โˆ– 1o) โ†” (๐ด โˆˆ On โˆง โˆ… โˆˆ ๐ด))
6259, 60, 61sylanbrc 584 . . . . . . . . 9 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ๐ด โˆˆ (On โˆ– 1o))
63 1onn 8587 . . . . . . . . . 10 1o โˆˆ ฯ‰
64 ondif2 8449 . . . . . . . . . 10 (ฯ‰ โˆˆ (On โˆ– 2o) โ†” (ฯ‰ โˆˆ On โˆง 1o โˆˆ ฯ‰))
6533, 63, 64mpbir2an 710 . . . . . . . . 9 ฯ‰ โˆˆ (On โˆ– 2o)
6662, 65jctil 521 . . . . . . . 8 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (ฯ‰ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ (On โˆ– 1o)))
6766adantr 482 . . . . . . 7 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โ†’ (ฯ‰ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ (On โˆ– 1o)))
68 oeeu 8551 . . . . . . 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 2572 . . . . . . 7 (โˆƒ!๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ โˆƒ๐‘คโˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)โˆƒ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด))
71 simpr 486 . . . . . . . . . . . 12 ((๐‘ค = โŸจ๐‘ฅ, ๐‘ฆ, ๐‘งโŸฉ โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด)
72 0ss 4357 . . . . . . . . . . . . . . . . . . 19 โˆ… โŠ† ๐‘ง
73 0elon 6372 . . . . . . . . . . . . . . . . . . . 20 โˆ… โˆˆ On
74 simpr 486 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ On)
75 oecl 8484 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
7633, 74, 75sylancr 588 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
7776ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
78 onelon 6343 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
7977, 78sylancom 589 . . . . . . . . . . . . . . . . . . . 20 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
80 1on 8425 . . . . . . . . . . . . . . . . . . . . . 22 1o โˆˆ On
81 omcl 8483 . . . . . . . . . . . . . . . . . . . . . 22 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง 1o โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
8276, 80, 81sylancl 587 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
8382ad5ant12 755 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
84 oaword 8497 . . . . . . . . . . . . . . . . . . . . 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 1469 . . . . . . . . . . . . . . . . . . 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 775 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o))
89 omsson 7807 . . . . . . . . . . . . . . . . . . . . . . 23 ฯ‰ โŠ† On
90 ssdif 4100 . . . . . . . . . . . . . . . . . . . . . . 23 (ฯ‰ โŠ† On โ†’ (ฯ‰ โˆ– 1o) โŠ† (On โˆ– 1o))
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (ฯ‰ โˆ– 1o) โŠ† (On โˆ– 1o)
9291sseli 3941 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o) โ†’ ๐‘ฆ โˆˆ (On โˆ– 1o))
93 ondif1 8448 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ (On โˆ– 1o) โ†” (๐‘ฆ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฆ))
94 df-1o 8413 . . . . . . . . . . . . . . . . . . . . . . 23 1o = suc โˆ…
95 eloni 6328 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ On โ†’ Ord ๐‘ฆ)
96 ordsucss 7754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord ๐‘ฆ โ†’ (โˆ… โˆˆ ๐‘ฆ โ†’ suc โˆ… โŠ† ๐‘ฆ))
9795, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฆ โ†’ suc โˆ… โŠ† ๐‘ฆ))
9897imp 408 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฆ โˆˆ On โˆง โˆ… โˆˆ ๐‘ฆ) โ†’ suc โˆ… โŠ† ๐‘ฆ)
9994, 98eqsstrid 3993 . . . . . . . . . . . . . . . . . . . . . 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 4087 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o) โ†’ ๐‘ฆ โˆˆ ฯ‰)
103 nnon 7809 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ ฯ‰ โ†’ ๐‘ฆ โˆˆ On)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o) โ†’ ๐‘ฆ โˆˆ On)
105104ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 (((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ฆ โˆˆ On)
106 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฅ โˆˆ On)
10733, 106, 75sylancr 588 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
108 omwordi 8519 . . . . . . . . . . . . . . . . . . . . 21 ((1o โˆˆ On โˆง ๐‘ฆ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (1o โŠ† ๐‘ฆ โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ)))
10980, 105, 107, 108mp3an2ani 1469 . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฆ โˆˆ On)
112 omcl 8483 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On)
113107, 111, 112syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) โˆˆ On)
11479adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ง โˆˆ On)
115 oawordri 8498 . . . . . . . . . . . . . . . . . . . 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 1372 . . . . . . . . . . . . . . . . . . 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 3955 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) +o โˆ…) โŠ† (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง))
11933, 75mpan 689 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ On โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
120119, 80, 81sylancl 587 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ On โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) โˆˆ On)
121 oa0 8463 . . . . . . . . . . . . . . . . . . . 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 8490 . . . . . . . . . . . . . . . . . . . 20 ((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) = (ฯ‰ โ†‘o ๐‘ฅ))
124119, 123syl 17 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ On โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo 1o) = (ฯ‰ โ†‘o ๐‘ฅ))
125122, 124eqtrd 2773 . . . . . . . . . . . . . . . . . 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 486 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด)
128118, 126, 1273sstr3d 3991 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โŠ† ๐ด)
129 simp-7l 788 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด โˆˆ ๐ต)
130 simplrl 776 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
131130ad4antr 731 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
132129, 131eleqtrd 2836 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
13355ad6antlr 736 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
134 ontr2 6365 . . . . . . . . . . . . . . . . 17 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) โŠ† ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
135107, 133, 134syl2anc 585 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) โŠ† ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
136128, 132, 135mp2and 698 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
13736ad6antlr 736 . . . . . . . . . . . . . . . 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 8536 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
140106, 137, 138, 139syl3anc 1372 . . . . . . . . . . . . . . 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 785 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ฯ‰ โŠ† ๐ด)
143142, 128unssd 4147 . . . . . . . . . . . . . 14 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด)
144 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
145 onelpss 6358 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ง โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†” (๐‘ง โŠ† (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ))))
146145biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ง โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (๐‘ง โŠ† (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ))))
14779, 107, 146syl2an2r 684 . . . . . . . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง โŠ† (ฯ‰ โ†‘o ๐‘ฅ) โˆง ๐‘ง โ‰  (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ ๐‘ง โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
150148, 149syl 17 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ง โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
151 oaword 8497 . . . . . . . . . . . . . . . . . . . 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 1372 . . . . . . . . . . . . . . . . . 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 8473 . . . . . . . . . . . . . . . . . 18 (((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ)))
156107, 111, 155syl2anc 585 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o (ฯ‰ โ†‘o ๐‘ฅ)))
157154, 156sseqtrrd 3986 . . . . . . . . . . . . . . . 16 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ))
158 ordom 7813 . . . . . . . . . . . . . . . . . . 19 Ord ฯ‰
15988, 102syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐‘ฆ โˆˆ ฯ‰)
160 ordsucss 7754 . . . . . . . . . . . . . . . . . . 19 (Ord ฯ‰ โ†’ (๐‘ฆ โˆˆ ฯ‰ โ†’ suc ๐‘ฆ โŠ† ฯ‰))
161158, 159, 160mpsyl 68 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ suc ๐‘ฆ โŠ† ฯ‰)
162 oe1 8492 . . . . . . . . . . . . . . . . . . . 20 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o 1o) = ฯ‰)
16333, 162ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (ฯ‰ โ†‘o 1o) = ฯ‰
164 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฅ = โˆ…)
165164oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o โˆ…))
166 oe0 8469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o โˆ…) = 1o)
16733, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ฯ‰ โ†‘o โˆ…) = 1o
168165, 167eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = 1o)
169168oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) = (1o ยทo ๐‘ฆ))
170104adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โ†’ ๐‘ฆ โˆˆ On)
171170ad5ant12 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฆ โˆˆ On)
172 om1r 8491 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฆ โˆˆ On โ†’ (1o ยทo ๐‘ฆ) = ๐‘ฆ)
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (1o ยทo ๐‘ฆ) = ๐‘ฆ)
174169, 173eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) = ๐‘ฆ)
175 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
176175, 168eleqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ง โˆˆ 1o)
177 el1o 8442 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ง โˆˆ 1o โ†” ๐‘ง = โˆ…)
178176, 177sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ง = โˆ…)
179174, 178oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = (๐‘ฆ +o โˆ…))
180 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด)
181 oa0 8463 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ โˆˆ On โ†’ (๐‘ฆ +o โˆ…) = ๐‘ฆ)
182171, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฆ +o โˆ…) = ๐‘ฆ)
183179, 180, 1823eqtr3d 2781 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐ด = ๐‘ฆ)
184159adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฆ โˆˆ ฯ‰)
185183, 184eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โˆง ๐‘ฅ = โˆ…) โ†’ ๐ด โˆˆ ฯ‰)
186185ex 414 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ฅ = โˆ… โ†’ ๐ด โˆˆ ฯ‰))
18733, 33pm3.2i 472 . . . . . . . . . . . . . . . . . . . . . . 23 (ฯ‰ โˆˆ On โˆง ฯ‰ โˆˆ On)
188 ontr2 6365 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ฯ‰ โˆˆ On โˆง ฯ‰ โˆˆ On) โ†’ ((ฯ‰ โŠ† ๐ด โˆง ๐ด โˆˆ ฯ‰) โ†’ ฯ‰ โˆˆ ฯ‰))
189188expd 417 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โˆˆ On โˆง ฯ‰ โˆˆ On) โ†’ (ฯ‰ โŠ† ๐ด โ†’ (๐ด โˆˆ ฯ‰ โ†’ ฯ‰ โˆˆ ฯ‰)))
190187, 142, 189mpsyl 68 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด โˆˆ ฯ‰ โ†’ ฯ‰ โˆˆ ฯ‰))
191 elirr 9538 . . . . . . . . . . . . . . . . . . . . . . . 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 6328 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ On โ†’ Ord ๐‘ฅ)
196 ordsucss 7754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord ๐‘ฅ โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ suc โˆ… โŠ† ๐‘ฅ))
197196imp 408 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Ord ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ suc โˆ… โŠ† ๐‘ฅ)
19894, 197eqsstrid 3993 . . . . . . . . . . . . . . . . . . . . . . 23 ((Ord ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ 1o โŠ† ๐‘ฅ)
199198ex 414 . . . . . . . . . . . . . . . . . . . . . 22 (Ord ๐‘ฅ โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ 1o โŠ† ๐‘ฅ))
200106, 195, 1993syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ 1o โŠ† ๐‘ฅ))
201 on0eqel 6442 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
202106, 201syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
203194, 200, 202mpjaod 859 . . . . . . . . . . . . . . . . . . . 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 1129 . . . . . . . . . . . . . . . . . . . . 21 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (1o โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ฯ‰ โˆˆ On))
207 oewordi 8539 . . . . . . . . . . . . . . . . . . . . 21 (((1o โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ฯ‰ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ (1o โŠ† ๐‘ฅ โ†’ (ฯ‰ โ†‘o 1o) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
208206, 39, 207sylancl 587 . . . . . . . . . . . . . . . . . . . 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 3994 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ฯ‰ โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
211161, 210sstrd 3955 . . . . . . . . . . . . . . . . 17 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ suc ๐‘ฆ โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
212 onsuc 7747 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ โˆˆ On โ†’ suc ๐‘ฆ โˆˆ On)
213111, 212syl 17 . . . . . . . . . . . . . . . . . 18 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ suc ๐‘ฆ โˆˆ On)
214 omwordi 8519 . . . . . . . . . . . . . . . . . 18 ((suc ๐‘ฆ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (suc ๐‘ฆ โŠ† (ฯ‰ โ†‘o ๐‘ฅ) โ†’ ((ฯ‰ โ†‘o ๐‘ฅ) ยทo suc ๐‘ฆ) โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ))))
215213, 107, 107, 214syl3anc 1372 . . . . . . . . . . . . . . . . 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 3955 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) โŠ† ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
218127eqcomd 2739 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด = (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง))
219 oeoa 8545 . . . . . . . . . . . . . . . 16 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
22033, 106, 106, 219mp3an2i 1467 . . . . . . . . . . . . . . 15 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
221217, 218, 2203sstr4d 3992 . . . . . . . . . . . . . 14 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))
222 simpr3 1197 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))
22359adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โˆˆ On)
224 simprr 772 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ๐ถ โˆˆ On)
225 simp1 1137 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ))
226224, 225anim12i 614 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)))
227 onelon 6343 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ ๐‘ฅ โˆˆ On)
22835, 227sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ ๐‘ฅ โˆˆ On)
229 pm4.24 565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ On โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On))
230228, 229sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On))
231 oacl 8482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฅ +o ๐‘ฅ) โˆˆ On)
232230, 231syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐‘ฅ +o ๐‘ฅ) โˆˆ On)
233 oecl 8484 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โˆˆ On โˆง (๐‘ฅ +o ๐‘ฅ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On)
23433, 232, 233sylancr 588 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On)
235226, 234syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On)
23655ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)
237 omwordri 8520 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด โˆˆ On โˆง (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On) โ†’ (๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โŠ† ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))))
238223, 235, 236, 237syl3anc 1372 . . . . . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
242 oeoa 8545 . . . . . . . . . . . . . . . . . . . . 21 ((ฯ‰ โˆˆ On โˆง (๐‘ฅ +o ๐‘ฅ) โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (ฯ‰ โ†‘o ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
24333, 240, 241, 242mp3an2i 1467 . . . . . . . . . . . . . . . . . . . 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 8509 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ)) = (๐‘ฅ +o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))))
246244, 244, 241, 245syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ)) = (๐‘ฅ +o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))))
247 simpr1 1195 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ))
248 ssidd 3968 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o ๐ถ) โŠ† (ฯ‰ โ†‘o ๐ถ))
249 oaabs2 8596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โˆง (ฯ‰ โ†‘o ๐ถ) โŠ† (ฯ‰ โ†‘o ๐ถ)) โ†’ (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
250247, 241, 248, 249syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
251250oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐‘ฅ +o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)))
252246, 251, 2503eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
253252oveq2d 7374 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o ((๐‘ฅ +o ๐‘ฅ) +o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
254243, 253eqtr3d 2775 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
255239, 254sseqtrd 3985 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โŠ† (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
256 oveq2 7366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o โˆ…))
257256, 167eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = 1o)
258257uneq2d 4124 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โˆช 1o))
25933oneluni 6437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1o โˆˆ ฯ‰ โ†’ (ฯ‰ โˆช 1o) = ฯ‰)
26063, 259ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ฯ‰ โˆช 1o) = ฯ‰
261260, 163eqtr4i 2764 . . . . . . . . . . . . . . . . . . . . . . . 24 (ฯ‰ โˆช 1o) = (ฯ‰ โ†‘o 1o)
262258, 261eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o 1o))
263262adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o 1o))
264263oveq1d 7373 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o 1o) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
265224ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ๐ถ โˆˆ On)
266 oecl 8484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((ฯ‰ โˆˆ On โˆง โˆ… โˆˆ On) โ†’ (ฯ‰ โ†‘o โˆ…) โˆˆ On)
26733, 73, 266mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ฯ‰ โ†‘o โˆ…) โˆˆ On
268 oecl 8484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o โˆ…) โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On)
26933, 267, 268mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On
2702692a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On))
271270, 54jca2 515 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On)))
272167oveq2i 7369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) = (ฯ‰ โ†‘o 1o)
273272, 163eqtri 2761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) = ฯ‰
274 ssun1 4133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ฯ‰ โŠ† (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ))
275273, 274eqsstri 3979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โŠ† (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ))
276 simp2 1138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด)
277275, 276sstrid 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โŠ† ๐ด)
278277adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โŠ† ๐ด)
27957ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โˆˆ ๐ต)
280 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
281279, 280eleqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
282278, 281jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โŠ† ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
283282adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โŠ† ๐ด โˆง ๐ด โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
284 ontr2 6365 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8536 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((โˆ… โˆˆ On โˆง ๐ถ โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (โˆ… โˆˆ ๐ถ โ†” (ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ)))
28773, 65, 286mp3an13 1453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†” (ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ)))
28865a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐ถ โˆˆ On โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
289 oeord 8536 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ฯ‰ โ†‘o โˆ…) โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ ((ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
290267, 35, 288, 289mp3an2i 1467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐ถ โˆˆ On โ†’ ((ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o ๐ถ) โ†” (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
291287, 290bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†” (ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
292291biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ถ โˆˆ On โ†’ ((ฯ‰ โ†‘o (ฯ‰ โ†‘o โˆ…)) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โ†’ โˆ… โˆˆ ๐ถ))
293285, 292sylcom 30 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ โˆ… โˆˆ ๐ถ))
294 eloni 6328 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ถ โˆˆ On โ†’ Ord ๐ถ)
295 ordsucss 7754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord ๐ถ โ†’ (โˆ… โˆˆ ๐ถ โ†’ suc โˆ… โŠ† ๐ถ))
29694sseq1i 3973 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1o โŠ† ๐ถ โ†” suc โˆ… โŠ† ๐ถ)
297295, 296syl6ibr 252 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord ๐ถ โ†’ (โˆ… โˆˆ ๐ถ โ†’ 1o โŠ† ๐ถ))
298294, 297syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ถ โˆˆ On โ†’ (โˆ… โˆˆ ๐ถ โ†’ 1o โŠ† ๐ถ))
299293, 298sylcom 30 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โ†’ 1o โŠ† ๐ถ))
300265, 299jcai 518 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง ๐‘ฅ = โˆ…) โ†’ (๐ถ โˆˆ On โˆง 1o โŠ† ๐ถ))
30133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ถ โˆˆ On โ†’ ฯ‰ โˆˆ On)
30280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ถ โˆˆ On โ†’ 1o โˆˆ On)
303301, 302, 353jca 1129 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ถ โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง 1o โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On))
304303adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ถ โˆˆ On โˆง 1o โŠ† ๐ถ) โ†’ (ฯ‰ โˆˆ On โˆง 1o โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On))
305 oeoa 8545 . . . . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ถ โˆˆ On โˆง 1o โŠ† ๐ถ) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
309 oeword 8538 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1o โˆˆ On โˆง ๐ถ โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (1o โŠ† ๐ถ โ†” (ฯ‰ โ†‘o 1o) โŠ† (ฯ‰ โ†‘o ๐ถ)))
31080, 65, 309mp3an13 1453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐ถ โˆˆ On โ†’ (1o โŠ† ๐ถ โ†” (ฯ‰ โ†‘o 1o) โŠ† (ฯ‰ โ†‘o ๐ถ)))
311310biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐ถ โˆˆ On โˆง 1o โŠ† ๐ถ) โ†’ (ฯ‰ โ†‘o 1o) โŠ† (ฯ‰ โ†‘o ๐ถ))
312163, 311eqsstrrid 3994 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ถ โˆˆ On โˆง 1o โŠ† ๐ถ) โ†’ ฯ‰ โŠ† (ฯ‰ โ†‘o ๐ถ))
313 oaabs 8595 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1o โˆˆ ฯ‰ โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โˆง ฯ‰ โŠ† (ฯ‰ โ†‘o ๐ถ)) โ†’ (1o +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
314307, 308, 312, 313syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ถ โˆˆ On โˆง 1o โŠ† ๐ถ) โ†’ (1o +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
315314oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ On โˆง 1o โŠ† ๐ถ) โ†’ (ฯ‰ โ†‘o (1o +o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
316306, 315eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . . . . 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 408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ suc โˆ… โŠ† ๐‘ฅ)
32194, 320eqsstrid 3993 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ 1o โŠ† ๐‘ฅ)
322247adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ))
323241, 322, 227syl2an2r 684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ On)
32465a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
325 oeword 8538 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1o โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (1o โŠ† ๐‘ฅ โ†” (ฯ‰ โ†‘o 1o) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
32680, 323, 324, 325mp3an2i 1467 . . . . . . . . . . . . . . . . . . . . . . . . 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 3994 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ฯ‰ โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
329 ssequn1 4141 . . . . . . . . . . . . . . . . . . . . . . 23 (ฯ‰ โŠ† (ฯ‰ โ†‘o ๐‘ฅ) โ†” (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ))
330328, 329sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ))
331330oveq1d 7373 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
332241adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o ๐ถ) โˆˆ On)
333 oeoa 8545 . . . . . . . . . . . . . . . . . . . . . 22 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ถ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
33433, 323, 332, 333mp3an2i 1467 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = ((ฯ‰ โ†‘o ๐‘ฅ) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
335 ssidd 3968 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o ๐ถ) โŠ† (ฯ‰ โ†‘o ๐ถ))
336322, 332, 335, 249syl21anc 837 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ)) = (ฯ‰ โ†‘o ๐ถ))
337336oveq2d 7374 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (ฯ‰ โ†‘o (๐‘ฅ +o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
338331, 334, 3373eqtr2d 2779 . . . . . . . . . . . . . . . . . . . 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 958 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
341276adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด)
34233, 228, 75sylancr 588 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
343342, 33jctil 521 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ)) โ†’ (ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On))
344 onun2 6426 . . . . . . . . . . . . . . . . . . . . . 22 ((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โˆˆ On)
345226, 343, 3443syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โˆˆ On)
346 omwordri 8520 . . . . . . . . . . . . . . . . . . . . 21 (((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โˆˆ On โˆง ๐ด โˆˆ On โˆง (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆˆ On) โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โ†’ ((ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) โŠ† (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))))
347345, 223, 236, 346syl3anc 1372 . . . . . . . . . . . . . . . . . . . 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 3984 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โŠ† (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))))
350255, 349eqssd 3962 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง (๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ)))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ))) = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)))
35149ad2antlr 726 . . . . . . . . . . . . . . . . 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 414 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (๐ด ยทo ๐ต) = ๐ต))
354353ad5antr 733 . . . . . . . . . . . . . 14 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ ((๐‘ฅ โˆˆ (ฯ‰ โ†‘o ๐ถ) โˆง (ฯ‰ โˆช (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† ๐ด โˆง ๐ด โŠ† (ฯ‰ โ†‘o (๐‘ฅ +o ๐‘ฅ))) โ†’ (๐ด ยทo ๐ต) = ๐ต))
355141, 143, 221, 354mp3and 1465 . . . . . . . . . . . . 13 ((((((((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โˆง ฯ‰ โŠ† ๐ด) โˆง ๐‘ฅ โˆˆ On) โˆง ๐‘ฆ โˆˆ (ฯ‰ โˆ– 1o)) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โˆง (((ฯ‰ โ†‘o ๐‘ฅ) ยทo ๐‘ฆ) +o ๐‘ง) = ๐ด) โ†’ (๐ด ยทo ๐ต) = ๐ต)
356355ex 414 . . . . . . . . . . . 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 1937 . . . . . . 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 6328 . . . . . . 7 (๐ด โˆˆ On โ†’ Ord ๐ด)
36559, 364syl 17 . . . . . 6 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ Ord ๐ด)
366 ordtri2or 6416 . . . . . 6 ((Ord ๐ด โˆง Ord ฯ‰) โ†’ (๐ด โˆˆ ฯ‰ โˆจ ฯ‰ โŠ† ๐ด))
367365, 158, 366sylancl 587 . . . . 5 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (๐ด โˆˆ ฯ‰ โˆจ ฯ‰ โŠ† ๐ด))
36851, 363, 367mpjaodan 958 . . . 4 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (๐ด ยทo ๐ต) = ๐ต)
369368ex 414 . . 3 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On) โ†’ (๐ด ยทo ๐ต) = ๐ต))
3706, 30, 3693jaod 1429 . 2 ((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ต = โˆ… โˆจ ๐ต = 2o โˆจ (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On)) โ†’ (๐ด ยทo ๐ต) = ๐ต))
371370imp 408 1 (((๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต = โˆ… โˆจ ๐ต = 2o โˆจ (๐ต = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ถ)) โˆง ๐ถ โˆˆ On))) โ†’ (๐ด ยทo ๐ต) = ๐ต)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆจ w3o 1087   โˆง w3a 1088   = wceq 1542  โˆƒwex 1782   โˆˆ wcel 2107  โˆƒ!weu 2563   โ‰  wne 2940  โˆƒwrex 3070   โˆ– cdif 3908   โˆช cun 3909   โŠ† wss 3911  โˆ…c0 4283  {cpr 4589  โŸจcotp 4595  Ord word 6317  Oncon0 6318  suc csuc 6320  (class class class)co 7358  ฯ‰com 7803  1oc1o 8406  2oc2o 8407   +o coa 8410   ยทo comu 8411   โ†‘o coe 8412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673  ax-reg 9533  ax-inf2 9582
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-ot 4596  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-omul 8418  df-oexp 8419
This theorem is referenced by:  omcl2  41711
  Copyright terms: Public domain W3C validator