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

Theorem oeordi 8583
Description: Ordering law for ordinal exponentiation. Proposition 8.33 of [TakeutiZaring] p. 67. (Contributed by NM, 5-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
Assertion
Ref Expression
oeordi ((๐ต โˆˆ On โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต)))

Proof of Theorem oeordi
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7410 . . . . 5 (๐‘ฅ = suc ๐ด โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o suc ๐ด))
21eleq2d 2811 . . . 4 (๐‘ฅ = suc ๐ด โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
32imbi2d 340 . . 3 (๐‘ฅ = suc ๐ด โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
4 oveq2 7410 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o ๐‘ฆ))
54eleq2d 2811 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)))
65imbi2d 340 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
7 oveq2 7410 . . . . 5 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o suc ๐‘ฆ))
87eleq2d 2811 . . . 4 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)))
98imbi2d 340 . . 3 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))))
10 oveq2 7410 . . . . 5 (๐‘ฅ = ๐ต โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o ๐ต))
1110eleq2d 2811 . . . 4 (๐‘ฅ = ๐ต โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต)))
1211imbi2d 340 . . 3 (๐‘ฅ = ๐ต โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต))))
13 eldifi 4119 . . . . . . . 8 (๐ถ โˆˆ (On โˆ– 2o) โ†’ ๐ถ โˆˆ On)
14 oecl 8533 . . . . . . . 8 ((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ On)
1513, 14sylan 579 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ On)
16 om1 8538 . . . . . . 7 ((๐ถ โ†‘o ๐ด) โˆˆ On โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) = (๐ถ โ†‘o ๐ด))
1715, 16syl 17 . . . . . 6 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) = (๐ถ โ†‘o ๐ด))
18 ondif2 8498 . . . . . . . . 9 (๐ถ โˆˆ (On โˆ– 2o) โ†” (๐ถ โˆˆ On โˆง 1o โˆˆ ๐ถ))
1918simprbi 496 . . . . . . . 8 (๐ถ โˆˆ (On โˆ– 2o) โ†’ 1o โˆˆ ๐ถ)
2019adantr 480 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ 1o โˆˆ ๐ถ)
2113adantr 480 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ๐ถ โˆˆ On)
22 simpr 484 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ๐ด โˆˆ On)
23 dif20el 8501 . . . . . . . . . 10 (๐ถ โˆˆ (On โˆ– 2o) โ†’ โˆ… โˆˆ ๐ถ)
2423adantr 480 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ โˆ… โˆˆ ๐ถ)
25 oen0 8582 . . . . . . . . 9 (((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ถ) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐ด))
2621, 22, 24, 25syl21anc 835 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐ด))
27 omordi 8562 . . . . . . . 8 (((๐ถ โˆˆ On โˆง (๐ถ โ†‘o ๐ด) โˆˆ On) โˆง โˆ… โˆˆ (๐ถ โ†‘o ๐ด)) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ)))
2821, 15, 26, 27syl21anc 835 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ)))
2920, 28mpd 15 . . . . . 6 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
3017, 29eqeltrrd 2826 . . . . 5 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
31 oesuc 8523 . . . . . 6 ((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐ด) = ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
3213, 31sylan 579 . . . . 5 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐ด) = ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
3330, 32eleqtrrd 2828 . . . 4 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))
3433expcom 413 . . 3 (๐ด โˆˆ On โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
35 oecl 8533 . . . . . . . . . . 11 ((๐ถ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ On)
3613, 35sylan 579 . . . . . . . . . 10 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ On)
37 om1 8538 . . . . . . . . . 10 ((๐ถ โ†‘o ๐‘ฆ) โˆˆ On โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) = (๐ถ โ†‘o ๐‘ฆ))
3836, 37syl 17 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) = (๐ถ โ†‘o ๐‘ฆ))
3919adantr 480 . . . . . . . . . 10 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ 1o โˆˆ ๐ถ)
4013adantr 480 . . . . . . . . . . 11 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ๐ถ โˆˆ On)
41 simpr 484 . . . . . . . . . . . 12 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ๐‘ฆ โˆˆ On)
4223adantr 480 . . . . . . . . . . . 12 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ โˆ… โˆˆ ๐ถ)
43 oen0 8582 . . . . . . . . . . . 12 (((๐ถ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โˆง โˆ… โˆˆ ๐ถ) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐‘ฆ))
4440, 41, 42, 43syl21anc 835 . . . . . . . . . . 11 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐‘ฆ))
45 omordi 8562 . . . . . . . . . . 11 (((๐ถ โˆˆ On โˆง (๐ถ โ†‘o ๐‘ฆ) โˆˆ On) โˆง โˆ… โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ)))
4640, 36, 44, 45syl21anc 835 . . . . . . . . . 10 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ)))
4739, 46mpd 15 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
4838, 47eqeltrrd 2826 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
49 oesuc 8523 . . . . . . . . 9 ((๐ถ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) = ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
5013, 49sylan 579 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) = ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
5148, 50eleqtrrd 2828 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))
52 onsuc 7793 . . . . . . . . 9 (๐‘ฆ โˆˆ On โ†’ suc ๐‘ฆ โˆˆ On)
53 oecl 8533 . . . . . . . . 9 ((๐ถ โˆˆ On โˆง suc ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) โˆˆ On)
5413, 52, 53syl2an 595 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) โˆˆ On)
55 ontr1 6401 . . . . . . . 8 ((๐ถ โ†‘o suc ๐‘ฆ) โˆˆ On โ†’ (((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โˆง (๐ถ โ†‘o ๐‘ฆ) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)))
5654, 55syl 17 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โˆง (๐ถ โ†‘o ๐‘ฆ) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)))
5751, 56mpan2d 691 . . . . . 6 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)))
5857expcom 413 . . . . 5 (๐‘ฆ โˆˆ On โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))))
5958adantr 480 . . . 4 ((๐‘ฆ โˆˆ On โˆง ๐ด โˆˆ ๐‘ฆ) โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))))
6059a2d 29 . . 3 ((๐‘ฆ โˆˆ On โˆง ๐ด โˆˆ ๐‘ฆ) โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))))
61 bi2.04 387 . . . . . 6 ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
6261ralbii 3085 . . . . 5 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
63 r19.21v 3171 . . . . 5 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
6462, 63bitri 275 . . . 4 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
65 limsuc 7832 . . . . . . . . . 10 (Lim ๐‘ฅ โ†’ (๐ด โˆˆ ๐‘ฅ โ†” suc ๐ด โˆˆ ๐‘ฅ))
6665biimpa 476 . . . . . . . . 9 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โ†’ suc ๐ด โˆˆ ๐‘ฅ)
67 elex 3485 . . . . . . . . . . . . 13 (suc ๐ด โˆˆ ๐‘ฅ โ†’ suc ๐ด โˆˆ V)
68 sucexb 7786 . . . . . . . . . . . . . 14 (๐ด โˆˆ V โ†” suc ๐ด โˆˆ V)
69 sucidg 6436 . . . . . . . . . . . . . 14 (๐ด โˆˆ V โ†’ ๐ด โˆˆ suc ๐ด)
7068, 69sylbir 234 . . . . . . . . . . . . 13 (suc ๐ด โˆˆ V โ†’ ๐ด โˆˆ suc ๐ด)
7167, 70syl 17 . . . . . . . . . . . 12 (suc ๐ด โˆˆ ๐‘ฅ โ†’ ๐ด โˆˆ suc ๐ด)
72 eleq2 2814 . . . . . . . . . . . . . 14 (๐‘ฆ = suc ๐ด โ†’ (๐ด โˆˆ ๐‘ฆ โ†” ๐ด โˆˆ suc ๐ด))
73 oveq2 7410 . . . . . . . . . . . . . . 15 (๐‘ฆ = suc ๐ด โ†’ (๐ถ โ†‘o ๐‘ฆ) = (๐ถ โ†‘o suc ๐ด))
7473eleq2d 2811 . . . . . . . . . . . . . 14 (๐‘ฆ = suc ๐ด โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
7572, 74imbi12d 344 . . . . . . . . . . . . 13 (๐‘ฆ = suc ๐ด โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†” (๐ด โˆˆ suc ๐ด โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
7675rspcv 3600 . . . . . . . . . . . 12 (suc ๐ด โˆˆ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐ด โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
7771, 76mpid 44 . . . . . . . . . . 11 (suc ๐ด โˆˆ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
7877anc2li 555 . . . . . . . . . 10 (suc ๐ด โˆˆ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (suc ๐ด โˆˆ ๐‘ฅ โˆง (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
7973eliuni 4994 . . . . . . . . . 10 ((suc ๐ด โˆˆ ๐‘ฅ โˆง (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
8078, 79syl6 35 . . . . . . . . 9 (suc ๐ด โˆˆ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ)))
8166, 80syl 17 . . . . . . . 8 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ)))
8281adantr 480 . . . . . . 7 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ)))
8313adantl 481 . . . . . . . . . 10 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ ๐ถ โˆˆ On)
84 simpl 482 . . . . . . . . . 10 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ Lim ๐‘ฅ)
8523adantl 481 . . . . . . . . . 10 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ โˆ… โˆˆ ๐ถ)
86 vex 3470 . . . . . . . . . . 11 ๐‘ฅ โˆˆ V
87 oelim 8530 . . . . . . . . . . 11 (((๐ถ โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
8886, 87mpanlr1 703 . . . . . . . . . 10 (((๐ถ โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
8983, 84, 85, 88syl21anc 835 . . . . . . . . 9 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
9089adantlr 712 . . . . . . . 8 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
9190eleq2d 2811 . . . . . . 7 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ)))
9282, 91sylibrd 259 . . . . . 6 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)))
9392ex 412 . . . . 5 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ))))
9493a2d 29 . . . 4 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ))))
9564, 94biimtrid 241 . . 3 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ))))
963, 6, 9, 12, 34, 60, 95tfindsg2 7845 . 2 ((๐ต โˆˆ On โˆง ๐ด โˆˆ ๐ต) โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต)))
9796impancom 451 1 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3053  Vcvv 3466   โˆ– cdif 3938  โˆ…c0 4315  โˆช ciun 4988  Oncon0 6355  Lim wlim 6356  suc csuc 6357  (class class class)co 7402  1oc1o 8455  2oc2o 8456   ยทo comu 8460   โ†‘o coe 8461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-oexp 8468
This theorem is referenced by:  oeord  8584  oecan  8585  oeworde  8589  oelimcl  8596  oeord2lim  42608  oeord2i  42609  omcl2  42632
  Copyright terms: Public domain W3C validator