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

Theorem omass 8580
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 7417 . . . . . 6 (๐‘ฅ = โˆ… โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo โˆ…))
2 oveq2 7417 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo โˆ…))
32oveq2d 7425 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo โˆ…)))
41, 3eqeq12d 2749 . . . . 5 (๐‘ฅ = โˆ… โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo โˆ…) = (๐ด ยทo (๐ต ยทo โˆ…))))
5 oveq2 7417 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo ๐‘ฆ))
6 oveq2 7417 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo ๐‘ฆ))
76oveq2d 7425 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
85, 7eqeq12d 2749 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
9 oveq2 7417 . . . . . 6 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ))
10 oveq2 7417 . . . . . . 7 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo suc ๐‘ฆ))
1110oveq2d 7425 . . . . . 6 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ)))
129, 11eqeq12d 2749 . . . . 5 (๐‘ฅ = suc ๐‘ฆ โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo suc ๐‘ฆ) = (๐ด ยทo (๐ต ยทo suc ๐‘ฆ))))
13 oveq2 7417 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = ((๐ด ยทo ๐ต) ยทo ๐ถ))
14 oveq2 7417 . . . . . . 7 (๐‘ฅ = ๐ถ โ†’ (๐ต ยทo ๐‘ฅ) = (๐ต ยทo ๐ถ))
1514oveq2d 7425 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ (๐ด ยทo (๐ต ยทo ๐‘ฅ)) = (๐ด ยทo (๐ต ยทo ๐ถ)))
1613, 15eqeq12d 2749 . . . . 5 (๐‘ฅ = ๐ถ โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (๐ด ยทo (๐ต ยทo ๐‘ฅ)) โ†” ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))))
17 omcl 8536 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
18 om0 8517 . . . . . . 7 ((๐ด ยทo ๐ต) โˆˆ On โ†’ ((๐ด ยทo ๐ต) ยทo โˆ…) = โˆ…)
1917, 18syl 17 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo โˆ…) = โˆ…)
20 om0 8517 . . . . . . . 8 (๐ต โˆˆ On โ†’ (๐ต ยทo โˆ…) = โˆ…)
2120oveq2d 7425 . . . . . . 7 (๐ต โˆˆ On โ†’ (๐ด ยทo (๐ต ยทo โˆ…)) = (๐ด ยทo โˆ…))
22 om0 8517 . . . . . . 7 (๐ด โˆˆ On โ†’ (๐ด ยทo โˆ…) = โˆ…)
2321, 22sylan9eqr 2795 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo (๐ต ยทo โˆ…)) = โˆ…)
2419, 23eqtr4d 2776 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) ยทo โˆ…) = (๐ด ยทo (๐ต ยทo โˆ…)))
25 oveq1 7416 . . . . . . . . 9 (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ (((๐ด ยทo ๐ต) ยทo ๐‘ฆ) +o (๐ด ยทo ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) +o (๐ด ยทo ๐ต)))
26 omsuc 8526 . . . . . . . . . . 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 8526 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต ยทo suc ๐‘ฆ) = ((๐ต ยทo ๐‘ฆ) +o ๐ต))
29283adant1 1131 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต ยทo suc ๐‘ฆ) = ((๐ต ยทo ๐‘ฆ) +o ๐ต))
3029oveq2d 7425 . . . . . . . . . . 11 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo (๐ต ยทo suc ๐‘ฆ)) = (๐ด ยทo ((๐ต ยทo ๐‘ฆ) +o ๐ต)))
31 omcl 8536 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ On)
32 odi 8579 . . . . . . . . . . . . . . . . 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 3479 . . . . . . . . . . . . . . 15 ๐‘ฅ โˆˆ V
47 omlim 8533 . . . . . . . . . . . . . . 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 5017 . . . . . . . . . . . 12 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ ((๐ด ยทo ๐ต) ยทo ๐‘ฆ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
53 limelon 6429 . . . . . . . . . . . . . . . . . . . . . 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 8566 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ (๐ต ยทo ๐‘ฅ)))
5856, 57sylan 581 . . . . . . . . . . . . . . . . . 18 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ (๐‘ฆ โˆˆ ๐‘ฅ โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ (๐ต ยทo ๐‘ฅ)))
59 ssid 4005 . . . . . . . . . . . . . . . . . . 19 (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))
60 oveq2 7417 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ง = (๐ต ยทo ๐‘ฆ) โ†’ (๐ด ยทo ๐‘ง) = (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
6160sseq2d 4015 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง = (๐ต ยทo ๐‘ฆ) โ†’ ((๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง) โ†” (๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ))))
6261rspcev 3613 . . . . . . . . . . . . . . . . . . 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 3146 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ฅ โˆƒ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo (๐ต ยทo ๐‘ฆ)) โŠ† (๐ด ยทo ๐‘ง))
66 iunss2 5053 . . . . . . . . . . . . . . . 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 8536 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ต ยทo ๐‘ฅ) โˆˆ On)
7054, 69sylan2 594 . . . . . . . . . . . . . . . . . . . 20 ((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โ†’ (๐ต ยทo ๐‘ฅ) โˆˆ On)
71 onelon 6390 . . . . . . . . . . . . . . . . . . . 20 (((๐ต ยทo ๐‘ฅ) โˆˆ On โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
7270, 71sylan 581 . . . . . . . . . . . . . . . . . . 19 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
7372adantlr 714 . . . . . . . . . . . . . . . . . 18 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
74 omordlim 8577 . . . . . . . . . . . . . . . . . . . . . . . 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 6390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ On)
7954, 78sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Lim ๐‘ฅ โˆง ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ ๐‘ฆ โˆˆ On)
8079, 31sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐ต โˆˆ On โˆง (Lim ๐‘ฅ โˆง ๐‘ฆ โˆˆ ๐‘ฅ)) โ†’ (๐ต ยทo ๐‘ฆ) โˆˆ On)
81 onelss 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐ต ยทo ๐‘ฆ) โˆˆ On โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ ๐‘ง โŠ† (๐ต ยทo ๐‘ฆ)))
82813ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘ง โˆˆ On โˆง (๐ต ยทo ๐‘ฆ) โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โˆˆ (๐ต ยทo ๐‘ฆ) โ†’ ๐‘ง โŠ† (๐ต ยทo ๐‘ฆ)))
83 omwordi 8571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3166 . . . . . . . . . . . . . . . . . . . . 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 3147 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ โˆ€๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)โˆƒ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo (๐ต ยทo ๐‘ฆ)))
97 iunss2 5053 . . . . . . . . . . . . . . . 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 4000 . . . . . . . . . . . . 13 ((((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ต) โ†’ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต ยทo ๐‘ฆ)) = โˆช ๐‘ง โˆˆ (๐ต ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง))
101 omlimcl 8578 . . . . . . . . . . . . . . . . 17 (((๐ต โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โˆง โˆ… โˆˆ ๐ต) โ†’ Lim (๐ต ยทo ๐‘ฅ))
10246, 101mpanlr1 705 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ต) โ†’ Lim (๐ต ยทo ๐‘ฅ))
103 ovex 7442 . . . . . . . . . . . . . . . . 17 (๐ต ยทo ๐‘ฅ) โˆˆ V
104 omlim 8533 . . . . . . . . . . . . . . . . 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 6375 . . . . . . . . . . . . 13 (๐ต โˆˆ On โ†’ Ord ๐ต)
114 ord0eln0 6420 . . . . . . . . . . . . . 14 (Ord ๐ต โ†’ (โˆ… โˆˆ ๐ต โ†” ๐ต โ‰  โˆ…))
115114necon2bbid 2985 . . . . . . . . . . . . 13 (Ord ๐ต โ†’ (๐ต = โˆ… โ†” ยฌ โˆ… โˆˆ ๐ต))
116113, 115syl 17 . . . . . . . . . . . 12 (๐ต โˆˆ On โ†’ (๐ต = โˆ… โ†” ยฌ โˆ… โˆˆ ๐ต))
117116ad2antrr 725 . . . . . . . . . . 11 (((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โˆง ๐ด โˆˆ On) โ†’ (๐ต = โˆ… โ†” ยฌ โˆ… โˆˆ ๐ต))
118 oveq2 7417 . . . . . . . . . . . . . . . . . . 19 (๐ต = โˆ… โ†’ (๐ด ยทo ๐ต) = (๐ด ยทo โˆ…))
119118, 22sylan9eqr 2795 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ On โˆง ๐ต = โˆ…) โ†’ (๐ด ยทo ๐ต) = โˆ…)
120119oveq1d 7424 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ On โˆง ๐ต = โˆ…) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = (โˆ… ยทo ๐‘ฅ))
121 om0r 8539 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ On โ†’ (โˆ… ยทo ๐‘ฅ) = โˆ…)
122120, 121sylan9eqr 2795 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ On โˆง (๐ด โˆˆ On โˆง ๐ต = โˆ…)) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆ…)
123122anassrs 469 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ On โˆง ๐ด โˆˆ On) โˆง ๐ต = โˆ…) โ†’ ((๐ด ยทo ๐ต) ยทo ๐‘ฅ) = โˆ…)
124 oveq1 7416 . . . . . . . . . . . . . . . . . . 19 (๐ต = โˆ… โ†’ (๐ต ยทo ๐‘ฅ) = (โˆ… ยทo ๐‘ฅ))
125124, 121sylan9eqr 2795 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ On โˆง ๐ต = โˆ…) โ†’ (๐ต ยทo ๐‘ฅ) = โˆ…)
126125oveq2d 7425 . . . . . . . . . . . . . . . . 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 7854 . . . 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 3062  โˆƒwrex 3071  Vcvv 3475   โŠ† wss 3949  โˆ…c0 4323  โˆช ciun 4998  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367  (class class class)co 7409   +o coa 8463   ยทo comu 8464
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-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-omul 8471
This theorem is referenced by:  oeoalem  8596  omabs  8650
  Copyright terms: Public domain W3C validator