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

Theorem omass 8531
Description: Multiplication of ordinal numbers is associative. Theorem 8.26 of [TakeutiZaring] p. 65. Theorem 4.4 of [Schloeder] p. 13. (Contributed by NM, 28-Dec-2004.)
Assertion
Ref Expression
omass ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))

Proof of Theorem omass
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7369 . . . . . 6 (๐‘ฅ = โˆ… โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo โˆ…))
2 oveq2 7369 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo โˆ…))
32oveq2d 7377 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo โˆ…)))
41, 3eqeq12d 2749 . . . . 5 (๐‘ฅ = โˆ… โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo โˆ…) = (๐ด ยทo (๐ต ยทo โˆ…))))
5 oveq2 7369 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo ๐‘ฆ))
6 oveq2 7369 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo ๐‘ฆ))
76oveq2d 7377 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
85, 7eqeq12d 2749 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
9 oveq2 7369 . . . . . 6 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ))
10 oveq2 7369 . . . . . . 7 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo suc ๐‘ฆ))
1110oveq2d 7377 . . . . . 6 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ)))
129, 11eqeq12d 2749 . . . . 5 (๐‘ฅ = suc ๐‘ฆ โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ))))
13 oveq2 7369 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo ๐ถ))
14 oveq2 7369 . . . . . . 7 (๐‘ฅ = ๐ถ โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo ๐ถ))
1514oveq2d 7377 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo ๐ถ)))
1613, 15eqeq12d 2749 . . . . 5 (๐‘ฅ = ๐ถ โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))))
17 omcl 8486 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
18 om0 8467 . . . . . . 7 ((๐ด ยทo ๐ต) โˆˆ On โ†’ ((๐ด ยทo ๐ต) ยทo โˆ…) = โˆ…)
1917, 18syl 17 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo โˆ…) = โˆ…)
20 om0 8467 . . . . . . . 8 (๐ต โˆˆ On โ†’ (๐ต ยทo โˆ…) = โˆ…)
2120oveq2d 7377 . . . . . . 7 (๐ต โˆˆ On โ†’ (๐ด ยทo (๐ต ยทo โˆ…)) = (๐ด ยทo โˆ…))
22 om0 8467 . . . . . . 7 (๐ด โˆˆ On โ†’ (๐ด ยทo โˆ…) = โˆ…)
2321, 22sylan9eqr 2795 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo (๐ต ยทo โˆ…)) = โˆ…)
2419, 23eqtr4d 2776 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo โˆ…) = (๐ด ยทo (๐ต ยทo โˆ…)))
25 oveq1 7368 . . . . . . . . 9 (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) +o (๐ด ยทo ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))
26 omsuc 8476 . . . . . . . . . . 11 (((๐ด ยทo ๐ต) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) +o (๐ด ยทo ๐ต)))
2717, 26stoic3 1779 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) +o (๐ด ยทo ๐ต)))
28 omsuc 8476 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต ยทo suc ๐‘ฆ) = ((๐ต ยทo ๐‘ฆ) +o ๐ต))
29283adant1 1131 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต ยทo suc ๐‘ฆ) = ((๐ต ยทo ๐‘ฆ) +o ๐ต))
3029oveq2d 7377 . . . . . . . . . . 11 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo (๐ต ยทo suc ๐‘ฆ)) = (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)))
31 omcl 8486 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ On)
32 odi 8530 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ On โˆง (๐ต ยทo ๐‘ฆ) โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))
3331, 32syl3an2 1165 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ On โˆง (๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))
34333exp 1120 . . . . . . . . . . . . . . 15 (๐ด โˆˆ On โ†’ ((๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต โˆˆ On โ†’ (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))))
3534expd 417 . . . . . . . . . . . . . 14 (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (๐‘ฆ โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต))))))
3635com34 91 . . . . . . . . . . . . 13 (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (๐‘ฆ โˆˆ On โ†’ (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต))))))
3736pm2.43d 53 . . . . . . . . . . . 12 (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (๐‘ฆ โˆˆ On โ†’ (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))))
38373imp 1112 . . . . . . . . . . 11 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))
3930, 38eqtrd 2773 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo (๐ต ยทo suc ๐‘ฆ)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))
4027, 39eqeq12d 2749 . . . . . . . . 9 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ)) โ†” (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) +o (๐ด ยทo ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต))))
4125, 40imbitrrid 245 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ))))
42413exp 1120 . . . . . . 7 (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (๐‘ฆ โˆˆ On โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ))))))
4342com3r 87 . . . . . 6 (๐‘ฆ โˆˆ On โ†’ (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ))))))
4443impd 412 . . . . 5 (๐‘ฆ โˆˆ On โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ)))))
4517ancoms 460 . . . . . . . . . . . . . 14 ((๐ต โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
46 vex 3451 . . . . . . . . . . . . . . 15 ๐‘ฅ โˆˆ V
47 omlim 8483 . . . . . . . . . . . . . . 15 (((๐ด ยทo ๐ต) โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ))
4846, 47mpanr1 702 . . . . . . . . . . . . . 14 (((๐ด ยทo ๐ต) โˆˆ On โˆง Lim ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ))
4945, 48sylan 581 . . . . . . . . . . . . 13 (((๐ต โˆˆ On โˆง ๐ด โˆˆ On) โˆง Lim ๐‘ฅ) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ))
5049an32s 651 . . . . . . . . . . . 12 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ))
5150ad2antrr 725 . . . . . . . . . . 11 (((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ))) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ))
52 iuneq2 4977 . . . . . . . . . . . 12 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
53 limelon 6385 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ On)
5446, 53mpan 689 . . . . . . . . . . . . . . . . . . . . 21 (Lim ๐‘ฅ โ†’ ๐‘ฅ โˆˆ On)
5554anim1i 616 . . . . . . . . . . . . . . . . . . . 20 ((Lim ๐‘ฅ โˆง ๐ต โˆˆ On) โ†’ (๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On))
5655ancoms 460 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โ†’ (๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On))
57 omordi 8517 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ (๐ต ยทo ๐‘ฅ)))
5856, 57sylan 581 . . . . . . . . . . . . . . . . . 18 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ (๐ต ยทo ๐‘ฅ)))
59 ssid 3970 . . . . . . . . . . . . . . . . . . 19 (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))
60 oveq2 7369 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ง = (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
6160sseq2d 3980 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง = (๐ต ยทo ๐‘ฆ) โ†’ ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง) โ†” (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
6261rspcev 3583 . . . . . . . . . . . . . . . . . . 19 (((๐ต ยทo ๐‘ฆ) โˆˆ (๐ต ยทo ๐‘ฅ) โˆง (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))) โ†’ โˆƒ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง))
6359, 62mpan2 690 . . . . . . . . . . . . . . . . . 18 ((๐ต ยทo ๐‘ฆ) โˆˆ (๐ต ยทo ๐‘ฅ) โ†’ โˆƒ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง))
6458, 63syl6 35 . . . . . . . . . . . . . . . . 17 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ โˆƒ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง)))
6564ralrimiv 3139 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ฅ โˆƒ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง))
66 iunss2 5013 . . . . . . . . . . . . . . . 16 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ โˆƒ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
6765, 66syl 17 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
6867adantlr 714 . . . . . . . . . . . . . 14 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
69 omcl 8486 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ต ยทo ๐‘ฅ) โˆˆ On)
7054, 69sylan2 594 . . . . . . . . . . . . . . . . . . . 20 ((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โ†’ (๐ต ยทo ๐‘ฅ) โˆˆ On)
71 onelon 6346 . . . . . . . . . . . . . . . . . . . 20 (((๐ต ยทo ๐‘ฅ) โˆˆ On โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
7270, 71sylan 581 . . . . . . . . . . . . . . . . . . 19 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
7372adantlr 714 . . . . . . . . . . . . . . . . . 18 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
74 omordlim 8528 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐ต โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ ๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ))
7574ex 414 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ต โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ ๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ)))
7646, 75mpanr1 702 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ ๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ)))
7776ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ง โˆˆ On โˆง (๐ต โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ ๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ)))
78 onelon 6346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ On)
7954, 78sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Lim ๐‘ฅ โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ On)
8079, 31sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐ต โˆˆ On โˆง (Lim ๐‘ฅ โˆง ๐‘ฆ โˆˆ ๐‘ฅ)) โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ On)
81 onelss 6363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐ต ยทo ๐‘ฆ) โˆˆ On โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ ๐‘ง โŠ† (๐ต ยทo ๐‘ฆ)))
82813ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘ง โˆˆ On โˆง (๐ต ยทo ๐‘ฆ) โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ ๐‘ง โŠ† (๐ต ยทo ๐‘ฆ)))
83 omwordi 8522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘ง โˆˆ On โˆง (๐ต ยทo ๐‘ฆ) โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โŠ† (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
8482, 83syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ง โˆˆ On โˆง (๐ต ยทo ๐‘ฆ) โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
85843exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ง โˆˆ On โ†’ ((๐ต ยทo ๐‘ฆ) โˆˆ On โ†’ (๐ด โˆˆ On โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))))
8680, 85syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ง โˆˆ On โ†’ ((๐ต โˆˆ On โˆง (Lim ๐‘ฅ โˆง ๐‘ฆ โˆˆ ๐‘ฅ)) โ†’ (๐ด โˆˆ On โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))))
8786exp4d 435 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ง โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (Lim ๐‘ฅ โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐ด โˆˆ On โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))))))
8887imp32 420 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ง โˆˆ On โˆง (๐ต โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐ด โˆˆ On โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))))
8988com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ง โˆˆ On โˆง (๐ต โˆˆ On โˆง Lim ๐‘ฅ)) โ†’ (๐ด โˆˆ On โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))))
9089imp 408 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ง โˆˆ On โˆง (๐ต โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐ด โˆˆ On) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ)))))
9190reximdvai 3159 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ง โˆˆ On โˆง (๐ต โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐ด โˆˆ On) โ†’ (โˆƒ๐‘ฆ โˆˆ ๐‘ฅ ๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
9277, 91syld 47 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ง โˆˆ On โˆง (๐ต โˆˆ On โˆง Lim ๐‘ฅ)) โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
9392exp31 421 . . . . . . . . . . . . . . . . . . 19 (๐‘ง โˆˆ On โ†’ ((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โ†’ (๐ด โˆˆ On โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))))
9493imp4c 425 . . . . . . . . . . . . . . . . . 18 (๐‘ง โˆˆ On โ†’ ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
9573, 94mpcom 38 . . . . . . . . . . . . . . . . 17 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
9695ralrimiva 3140 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ โˆ€๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
97 iunss2 5013 . . . . . . . . . . . . . . . 16 (โˆ€๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
9896, 97syl 17 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
9998adantr 482 . . . . . . . . . . . . . 14 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
10068, 99eqssd 3965 . . . . . . . . . . . . 13 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)) = โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
101 omlimcl 8529 . . . . . . . . . . . . . . . . 17 (((๐ต โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โˆง โˆ… โˆˆ ๐ต) โ†’ Lim (๐ต ยทo ๐‘ฅ))
10246, 101mpanlr1 705 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ Lim (๐ต ยทo ๐‘ฅ))
103 ovex 7394 . . . . . . . . . . . . . . . . 17 (๐ต ยทo ๐‘ฅ) โˆˆ V
104 omlim 8483 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ On โˆง ((๐ต ยทo ๐‘ฅ) โˆˆ V โˆง Lim (๐ต ยทo ๐‘ฅ))) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
105103, 104mpanr1 702 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ On โˆง Lim (๐ต ยทo ๐‘ฅ)) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
106102, 105sylan2 594 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง ((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต)) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
107106ancoms 460 . . . . . . . . . . . . . 14 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โˆง ๐ด โˆˆ On) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
108107an32s 651 . . . . . . . . . . . . 13 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
109100, 108eqtr4d 2776 . . . . . . . . . . . 12 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)))
11052, 109sylan9eqr 2795 . . . . . . . . . . 11 (((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ))) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)))
11151, 110eqtrd 2773 . . . . . . . . . 10 (((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ))) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)))
112111exp31 421 . . . . . . . . 9 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ (โˆ… โˆˆ ๐ต โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)))))
113 eloni 6331 . . . . . . . . . . . . 13 (๐ต โˆˆ On โ†’ Ord ๐ต)
114 ord0eln0 6376 . . . . . . . . . . . . . 14 (Ord ๐ต โ†’ (โˆ… โˆˆ ๐ต โ†” ๐ต โ‰  โˆ…))
115114necon2bbid 2984 . . . . . . . . . . . . 13 (Ord ๐ต โ†’ (๐ต = โˆ… โ†” ยฌ โˆ… โˆˆ ๐ต))
116113, 115syl 17 . . . . . . . . . . . 12 (๐ต โˆˆ On โ†’ (๐ต = โˆ… โ†” ยฌ โˆ… โˆˆ ๐ต))
117116ad2antrr 725 . . . . . . . . . . 11 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ (๐ต = โˆ… โ†” ยฌ โˆ… โˆˆ ๐ต))
118 oveq2 7369 . . . . . . . . . . . . . . . . . . 19 (๐ต = โˆ… โ†’ (๐ด ยทo ๐ต) = (๐ด ยทo โˆ…))
119118, 22sylan9eqr 2795 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ On โˆง ๐ต = โˆ…) โ†’ (๐ด ยทo ๐ต) = โˆ…)
120119oveq1d 7376 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ On โˆง ๐ต = โˆ…) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (โˆ… ยทo ๐‘ฅ))
121 om0r 8489 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ On โ†’ (โˆ… ยทo ๐‘ฅ) = โˆ…)
122120, 121sylan9eqr 2795 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ On โˆง (๐ด โˆˆ On โˆง ๐ต = โˆ…)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆ…)
123122anassrs 469 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โˆง ๐ต = โˆ…) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆ…)
124 oveq1 7368 . . . . . . . . . . . . . . . . . . 19 (๐ต = โˆ… โ†’ (๐ต ยทo ๐‘ฅ) = (โˆ… ยทo ๐‘ฅ))
125124, 121sylan9eqr 2795 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐ต = โˆ…) โ†’ (๐ต ยทo ๐‘ฅ) = โˆ…)
126125oveq2d 7377 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ On โˆง ๐ต = โˆ…) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo โˆ…))
127126, 22sylan9eq 2793 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ On โˆง ๐ต = โˆ…) โˆง ๐ด โˆˆ On) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = โˆ…)
128127an32s 651 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โˆง ๐ต = โˆ…) โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = โˆ…)
129123, 128eqtr4d 2776 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โˆง ๐ต = โˆ…) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)))
130129ex 414 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ต = โˆ… โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ))))
13154, 130sylan 581 . . . . . . . . . . . 12 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐ต = โˆ… โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ))))
132131adantll 713 . . . . . . . . . . 11 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ (๐ต = โˆ… โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ))))
133117, 132sylbird 260 . . . . . . . . . 10 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ (ยฌ โˆ… โˆˆ ๐ต โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ))))
134133a1dd 50 . . . . . . . . 9 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ (ยฌ โˆ… โˆˆ ๐ต โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)))))
135112, 134pm2.61d 179 . . . . . . . 8 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ))))
136135exp31 421 . . . . . . 7 (๐ต โˆˆ On โ†’ (Lim ๐‘ฅ โ†’ (๐ด โˆˆ On โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ))))))
137136com3l 89 . . . . . 6 (Lim ๐‘ฅ โ†’ (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ))))))
138137impd 412 . . . . 5 (Lim ๐‘ฅ โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)))))
1394, 8, 12, 16, 24, 44, 138tfinds3 7805 . . . 4 (๐ถ โˆˆ On โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))))
140139expd 417 . . 3 (๐ถ โˆˆ On โ†’ (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))))
141140com3l 89 . 2 (๐ด โˆˆ On โ†’ (๐ต โˆˆ On โ†’ (๐ถ โˆˆ On โ†’ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))))
1421413imp 1112 1 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ถ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3061  โˆƒwrex 3070  Vcvv 3447   โŠ† wss 3914  โˆ…c0 4286  โˆช ciun 4958  Ord word 6320  Oncon0 6321  Lim wlim 6322  suc csuc 6323  (class class class)co 7361   +o coa 8413   ยทo comu 8414
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 5246  ax-sep 5260  ax-nul 5267  ax-pr 5388  ax-un 7676
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 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-oadd 8420  df-omul 8421
This theorem is referenced by:  oeoalem  8547  omabs  8601
  Copyright terms: Public domain W3C validator