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

Theorem omabs 8650
Description: Ordinal multiplication is also absorbed by powers of ฯ‰. (Contributed by Mario Carneiro, 30-May-2015.)
Assertion
Ref Expression
omabs (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))

Proof of Theorem omabs
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2823 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (โˆ… โˆˆ ๐‘ฅ โ†” โˆ… โˆˆ โˆ…))
2 oveq2 7417 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o โˆ…))
32oveq2d 7425 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (๐ด ยทo (ฯ‰ โ†‘o โˆ…)))
43, 2eqeq12d 2749 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ) โ†” (๐ด ยทo (ฯ‰ โ†‘o โˆ…)) = (ฯ‰ โ†‘o โˆ…)))
51, 4imbi12d 345 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ ((โˆ… โˆˆ ๐‘ฅ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ)) โ†” (โˆ… โˆˆ โˆ… โ†’ (๐ด ยทo (ฯ‰ โ†‘o โˆ…)) = (ฯ‰ โ†‘o โˆ…))))
6 eleq2 2823 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ (โˆ… โˆˆ ๐‘ฅ โ†” โˆ… โˆˆ ๐‘ฆ))
7 oveq2 7417 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o ๐‘ฆ))
87oveq2d 7425 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)))
98, 7eqeq12d 2749 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ) โ†” (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)))
106, 9imbi12d 345 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ ((โˆ… โˆˆ ๐‘ฅ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ)) โ†” (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))))
11 eleq2 2823 . . . . . . . 8 (๐‘ฅ = suc ๐‘ฆ โ†’ (โˆ… โˆˆ ๐‘ฅ โ†” โˆ… โˆˆ suc ๐‘ฆ))
12 oveq2 7417 . . . . . . . . . 10 (๐‘ฅ = suc ๐‘ฆ โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o suc ๐‘ฆ))
1312oveq2d 7425 . . . . . . . . 9 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)))
1413, 12eqeq12d 2749 . . . . . . . 8 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ) โ†” (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ)))
1511, 14imbi12d 345 . . . . . . 7 (๐‘ฅ = suc ๐‘ฆ โ†’ ((โˆ… โˆˆ ๐‘ฅ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ)) โ†” (โˆ… โˆˆ suc ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ))))
16 eleq2 2823 . . . . . . . 8 (๐‘ฅ = ๐ต โ†’ (โˆ… โˆˆ ๐‘ฅ โ†” โˆ… โˆˆ ๐ต))
17 oveq2 7417 . . . . . . . . . 10 (๐‘ฅ = ๐ต โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = (ฯ‰ โ†‘o ๐ต))
1817oveq2d 7425 . . . . . . . . 9 (๐‘ฅ = ๐ต โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (๐ด ยทo (ฯ‰ โ†‘o ๐ต)))
1918, 17eqeq12d 2749 . . . . . . . 8 (๐‘ฅ = ๐ต โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ) โ†” (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต)))
2016, 19imbi12d 345 . . . . . . 7 (๐‘ฅ = ๐ต โ†’ ((โˆ… โˆˆ ๐‘ฅ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ)) โ†” (โˆ… โˆˆ ๐ต โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))))
21 noel 4331 . . . . . . . . 9 ยฌ โˆ… โˆˆ โˆ…
2221pm2.21i 119 . . . . . . . 8 (โˆ… โˆˆ โˆ… โ†’ (๐ด ยทo (ฯ‰ โ†‘o โˆ…)) = (ฯ‰ โ†‘o โˆ…))
2322a1i 11 . . . . . . 7 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โ†’ (โˆ… โˆˆ โˆ… โ†’ (๐ด ยทo (ฯ‰ โ†‘o โˆ…)) = (ฯ‰ โ†‘o โˆ…)))
24 simprl 770 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ฯ‰ โˆˆ On)
25 simpll 766 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ๐ด โˆˆ ฯ‰)
26 simplr 768 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ โˆ… โˆˆ ๐ด)
27 omabslem 8649 . . . . . . . . . . . . . . . 16 ((ฯ‰ โˆˆ On โˆง ๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo ฯ‰) = ฯ‰)
2824, 25, 26, 27syl3anc 1372 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (๐ด ยทo ฯ‰) = ฯ‰)
2928adantr 482 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โˆง ๐‘ฆ = โˆ…) โ†’ (๐ด ยทo ฯ‰) = ฯ‰)
30 suceq 6431 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ = โˆ… โ†’ suc ๐‘ฆ = suc โˆ…)
31 df-1o 8466 . . . . . . . . . . . . . . . . . 18 1o = suc โˆ…
3230, 31eqtr4di 2791 . . . . . . . . . . . . . . . . 17 (๐‘ฆ = โˆ… โ†’ suc ๐‘ฆ = 1o)
3332oveq2d 7425 . . . . . . . . . . . . . . . 16 (๐‘ฆ = โˆ… โ†’ (ฯ‰ โ†‘o suc ๐‘ฆ) = (ฯ‰ โ†‘o 1o))
34 oe1 8544 . . . . . . . . . . . . . . . . 17 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o 1o) = ฯ‰)
3534ad2antrl 727 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (ฯ‰ โ†‘o 1o) = ฯ‰)
3633, 35sylan9eqr 2795 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โˆง ๐‘ฆ = โˆ…) โ†’ (ฯ‰ โ†‘o suc ๐‘ฆ) = ฯ‰)
3736oveq2d 7425 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โˆง ๐‘ฆ = โˆ…) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (๐ด ยทo ฯ‰))
3829, 37, 363eqtr4d 2783 . . . . . . . . . . . . 13 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โˆง ๐‘ฆ = โˆ…) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ))
3938ex 414 . . . . . . . . . . . 12 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (๐‘ฆ = โˆ… โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ)))
4039a1dd 50 . . . . . . . . . . 11 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (๐‘ฆ = โˆ… โ†’ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ))))
41 oveq1 7416 . . . . . . . . . . . . . 14 ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) ยทo ฯ‰) = ((ฯ‰ โ†‘o ๐‘ฆ) ยทo ฯ‰))
42 oesuc 8527 . . . . . . . . . . . . . . . . . 18 ((ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (ฯ‰ โ†‘o suc ๐‘ฆ) = ((ฯ‰ โ†‘o ๐‘ฆ) ยทo ฯ‰))
4342adantl 483 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (ฯ‰ โ†‘o suc ๐‘ฆ) = ((ฯ‰ โ†‘o ๐‘ฆ) ยทo ฯ‰))
4443oveq2d 7425 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (๐ด ยทo ((ฯ‰ โ†‘o ๐‘ฆ) ยทo ฯ‰)))
45 nnon 7861 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ ฯ‰ โ†’ ๐ด โˆˆ On)
4645ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ๐ด โˆˆ On)
47 oecl 8537 . . . . . . . . . . . . . . . . . 18 ((ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ On)
4847adantl 483 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ On)
49 omass 8580 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ On โˆง ฯ‰ โˆˆ On) โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) ยทo ฯ‰) = (๐ด ยทo ((ฯ‰ โ†‘o ๐‘ฆ) ยทo ฯ‰)))
5046, 48, 24, 49syl3anc 1372 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) ยทo ฯ‰) = (๐ด ยทo ((ฯ‰ โ†‘o ๐‘ฆ) ยทo ฯ‰)))
5144, 50eqtr4d 2776 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) ยทo ฯ‰))
5251, 43eqeq12d 2749 . . . . . . . . . . . . . 14 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ((๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ) โ†” ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) ยทo ฯ‰) = ((ฯ‰ โ†‘o ๐‘ฆ) ยทo ฯ‰)))
5341, 52imbitrrid 245 . . . . . . . . . . . . 13 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ)))
5453imim2d 57 . . . . . . . . . . . 12 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ))))
5554com23 86 . . . . . . . . . . 11 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (โˆ… โˆˆ ๐‘ฆ โ†’ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ))))
56 simprr 772 . . . . . . . . . . . 12 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ๐‘ฆ โˆˆ On)
57 on0eqel 6489 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ On โ†’ (๐‘ฆ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฆ))
5856, 57syl 17 . . . . . . . . . . 11 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ (๐‘ฆ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฆ))
5940, 55, 58mpjaod 859 . . . . . . . . . 10 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ)))
6059a1dd 50 . . . . . . . . 9 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐‘ฆ โˆˆ On)) โ†’ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (โˆ… โˆˆ suc ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ))))
6160anassrs 469 . . . . . . . 8 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โˆง ๐‘ฆ โˆˆ On) โ†’ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (โˆ… โˆˆ suc ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ))))
6261expcom 415 . . . . . . 7 (๐‘ฆ โˆˆ On โ†’ (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โ†’ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (โˆ… โˆˆ suc ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o suc ๐‘ฆ)) = (ฯ‰ โ†‘o suc ๐‘ฆ)))))
6345ad3antrrr 729 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐ด โˆˆ On)
64 simprl 770 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ ฯ‰ โˆˆ On)
65 simprr 772 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ Lim ๐‘ฅ)
66 vex 3479 . . . . . . . . . . . . . . . . . 18 ๐‘ฅ โˆˆ V
6765, 66jctil 521 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ))
68 limelon 6429 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ On)
6967, 68syl 17 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ On)
70 oecl 8537 . . . . . . . . . . . . . . . 16 ((ฯ‰ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
7164, 69, 70syl2anc 585 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
7271adantr 482 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
73 1onn 8639 . . . . . . . . . . . . . . . . 17 1o โˆˆ ฯ‰
74 ondif2 8502 . . . . . . . . . . . . . . . . 17 (ฯ‰ โˆˆ (On โˆ– 2o) โ†” (ฯ‰ โˆˆ On โˆง 1o โˆˆ ฯ‰))
7564, 73, 74sylanblrc 591 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
7675adantr 482 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
7767adantr 482 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ))
78 oelimcl 8600 . . . . . . . . . . . . . . 15 ((ฯ‰ โˆˆ (On โˆ– 2o) โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โ†’ Lim (ฯ‰ โ†‘o ๐‘ฅ))
7976, 77, 78syl2anc 585 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ Lim (ฯ‰ โ†‘o ๐‘ฅ))
80 omlim 8533 . . . . . . . . . . . . . 14 ((๐ด โˆˆ On โˆง ((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง Lim (ฯ‰ โ†‘o ๐‘ฅ))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = โˆช ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐ด ยทo ๐‘ง))
8163, 72, 79, 80syl12anc 836 . . . . . . . . . . . . 13 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = โˆช ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐ด ยทo ๐‘ง))
82 simplrl 776 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ฯ‰ โˆˆ On)
83 oelim2 8595 . . . . . . . . . . . . . . . . . . . 20 ((ฯ‰ โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฆ))
8482, 77, 83syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฆ))
8584eleq2d 2820 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†” ๐‘ง โˆˆ โˆช ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฆ)))
86 eliun 5002 . . . . . . . . . . . . . . . . . 18 (๐‘ง โˆˆ โˆช ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)(ฯ‰ โ†‘o ๐‘ฆ) โ†” โˆƒ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))
8785, 86bitrdi 287 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†” โˆƒ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)))
8869adantr 482 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐‘ฅ โˆˆ On)
89 anass 470 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฆ โˆˆ ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†” (๐‘ฆ โˆˆ ๐‘ฅ โˆง (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))))
90 onelon 6390 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ On)
91 on0eln0 6421 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ฆ โ†” ๐‘ฆ โ‰  โˆ…))
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ (โˆ… โˆˆ ๐‘ฆ โ†” ๐‘ฆ โ‰  โˆ…))
9392pm5.32da 580 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ On โ†’ ((๐‘ฆ โˆˆ ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฆ) โ†” (๐‘ฆ โˆˆ ๐‘ฅ โˆง ๐‘ฆ โ‰  โˆ…)))
94 dif1o 8500 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o) โ†” (๐‘ฆ โˆˆ ๐‘ฅ โˆง ๐‘ฆ โ‰  โˆ…))
9593, 94bitr4di 289 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ On โ†’ ((๐‘ฆ โˆˆ ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฆ) โ†” ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)))
9695anbi1d 631 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ On โ†’ (((๐‘ฆ โˆˆ ๐‘ฅ โˆง โˆ… โˆˆ ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†” (๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))))
9789, 96bitr3id 285 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ On โ†’ ((๐‘ฆ โˆˆ ๐‘ฅ โˆง (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†” (๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))))
9897rexbidv2 3175 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ On โ†’ (โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†” โˆƒ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)))
9988, 98syl 17 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†” โˆƒ๐‘ฆ โˆˆ (๐‘ฅ โˆ– 1o)๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)))
10087, 99bitr4d 282 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†” โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))))
101 r19.29 3115 . . . . . . . . . . . . . . . . . 18 ((โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))))
102 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)))
103102imp 408 . . . . . . . . . . . . . . . . . . . . . 22 (((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง โˆ… โˆˆ ๐‘ฆ) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))
104103anim1i 616 . . . . . . . . . . . . . . . . . . . . 21 ((((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง โˆ… โˆˆ ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)))
105104anasss 468 . . . . . . . . . . . . . . . . . . . 20 (((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)))
10671ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On)
107 eloni 6375 . . . . . . . . . . . . . . . . . . . . . . 23 ((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โ†’ Ord (ฯ‰ โ†‘o ๐‘ฅ))
108106, 107syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ Ord (ฯ‰ โ†‘o ๐‘ฅ))
109 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))
11064ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ฯ‰ โˆˆ On)
11169ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐‘ฅ โˆˆ On)
112 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐‘ฆ โˆˆ ๐‘ฅ)
113111, 112, 90syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐‘ฆ โˆˆ On)
114110, 113, 47syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ On)
115 onelon 6390 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((ฯ‰ โ†‘o ๐‘ฆ) โˆˆ On โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ ๐‘ง โˆˆ On)
116114, 109, 115syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐‘ง โˆˆ On)
11745ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ ๐ด โˆˆ On)
118117ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ๐ด โˆˆ On)
119 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ โˆ… โˆˆ ๐ด)
120119ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ โˆ… โˆˆ ๐ด)
121 omord2 8567 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐‘ง โˆˆ On โˆง (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ) โ†” (๐ด ยทo ๐‘ง) โˆˆ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ))))
122116, 114, 118, 120, 121syl31anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ) โ†” (๐ด ยทo ๐‘ง) โˆˆ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ))))
123109, 122mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo ๐‘ง) โˆˆ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)))
124 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))
125123, 124eleqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo ๐‘ง) โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))
12675ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ ฯ‰ โˆˆ (On โˆ– 2o))
127 oeord 8588 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฆ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†” (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)))
128113, 111, 126, 127syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†” (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)))
129112, 128mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
130 ontr1 6411 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โ†’ (((๐ด ยทo ๐‘ง) โˆˆ (ฯ‰ โ†‘o ๐‘ฆ) โˆง (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ (๐ด ยทo ๐‘ง) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)))
131106, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (((๐ด ยทo ๐‘ง) โˆˆ (ฯ‰ โ†‘o ๐‘ฆ) โˆง (ฯ‰ โ†‘o ๐‘ฆ) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ (๐ด ยทo ๐‘ง) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)))
132125, 129, 131mp2and 698 . . . . . . . . . . . . . . . . . . . . . 22 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo ๐‘ง) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ))
133 ordelss 6381 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord (ฯ‰ โ†‘o ๐‘ฅ) โˆง (๐ด ยทo ๐‘ง) โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
134108, 132, 133syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โˆง ((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
135134ex 414 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ (((๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ) โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
136105, 135syl5 34 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ (((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
137136rexlimdva 3156 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ (โˆƒ๐‘ฆ โˆˆ ๐‘ฅ ((โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
138101, 137syl5 34 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ ((โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โˆง โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
139138expdimp 454 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โˆง ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
140100, 139sylbid 239 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ)))
141140ralrimiv 3146 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ โˆ€๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
142 iunss 5049 . . . . . . . . . . . . . 14 (โˆช ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ) โ†” โˆ€๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
143141, 142sylibr 233 . . . . . . . . . . . . 13 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ โˆช ๐‘ง โˆˆ (ฯ‰ โ†‘o ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
14481, 143eqsstrd 4021 . . . . . . . . . . . 12 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) โŠ† (ฯ‰ โ†‘o ๐‘ฅ))
145 simpllr 775 . . . . . . . . . . . . 13 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ โˆ… โˆˆ ๐ด)
146 omword2 8574 . . . . . . . . . . . . 13 ((((ฯ‰ โ†‘o ๐‘ฅ) โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โŠ† (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
14772, 63, 145, 146syl21anc 837 . . . . . . . . . . . 12 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (ฯ‰ โ†‘o ๐‘ฅ) โŠ† (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)))
148144, 147eqssd 4000 . . . . . . . . . . 11 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ))) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ))
149148ex 414 . . . . . . . . . 10 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ)))
150149anassrs 469 . . . . . . . . 9 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โˆง Lim ๐‘ฅ) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ)))
151150a1dd 50 . . . . . . . 8 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โˆง Lim ๐‘ฅ) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ))))
152151expcom 415 . . . . . . 7 (Lim ๐‘ฅ โ†’ (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (โˆ… โˆˆ ๐‘ฆ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฆ)) = (ฯ‰ โ†‘o ๐‘ฆ)) โ†’ (โˆ… โˆˆ ๐‘ฅ โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐‘ฅ)) = (ฯ‰ โ†‘o ๐‘ฅ)))))
1535, 10, 15, 20, 23, 62, 152tfinds3 7854 . . . . . 6 (๐ต โˆˆ On โ†’ (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ต โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))))
154153com12 32 . . . . 5 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง ฯ‰ โˆˆ On) โ†’ (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))))
155154adantrr 716 . . . 4 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On)) โ†’ (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))))
156155imp32 420 . . 3 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On)) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))
157156an32s 651 . 2 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โˆง (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))
158 nnm0 8605 . . . 4 (๐ด โˆˆ ฯ‰ โ†’ (๐ด ยทo โˆ…) = โˆ…)
159158ad3antrrr 729 . . 3 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โˆง ยฌ (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On)) โ†’ (๐ด ยทo โˆ…) = โˆ…)
160 fnoe 8510 . . . . . . 7 โ†‘o Fn (On ร— On)
161 fndm 6653 . . . . . . 7 ( โ†‘o Fn (On ร— On) โ†’ dom โ†‘o = (On ร— On))
162160, 161ax-mp 5 . . . . . 6 dom โ†‘o = (On ร— On)
163162ndmov 7591 . . . . 5 (ยฌ (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ต) = โˆ…)
164163adantl 483 . . . 4 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โˆง ยฌ (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On)) โ†’ (ฯ‰ โ†‘o ๐ต) = โˆ…)
165164oveq2d 7425 . . 3 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โˆง ยฌ (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (๐ด ยทo โˆ…))
166159, 165, 1643eqtr4d 2783 . 2 ((((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โˆง ยฌ (ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))
167157, 166pm2.61dan 812 1 (((๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ต โˆˆ On โˆง โˆ… โˆˆ ๐ต)) โ†’ (๐ด ยทo (ฯ‰ โ†‘o ๐ต)) = (ฯ‰ โ†‘o ๐ต))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  โˆ€wral 3062  โˆƒwrex 3071  Vcvv 3475   โˆ– cdif 3946   โŠ† wss 3949  โˆ…c0 4323  โˆช ciun 4998   ร— cxp 5675  dom cdm 5677  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367   Fn wfn 6539  (class class class)co 7409  ฯ‰com 7855  1oc1o 8459  2oc2o 8460   ยทo comu 8464   โ†‘o coe 8465
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 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-omul 8471  df-oexp 8472
This theorem is referenced by:  cnfcom3  9699  omabs2  42082
  Copyright terms: Public domain W3C validator