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

Theorem oeordi 8586
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 7416 . . . . 5 (๐‘ฅ = suc ๐ด โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o suc ๐ด))
21eleq2d 2819 . . . 4 (๐‘ฅ = suc ๐ด โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
32imbi2d 340 . . 3 (๐‘ฅ = suc ๐ด โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
4 oveq2 7416 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o ๐‘ฆ))
54eleq2d 2819 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)))
65imbi2d 340 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
7 oveq2 7416 . . . . 5 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o suc ๐‘ฆ))
87eleq2d 2819 . . . 4 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)))
98imbi2d 340 . . 3 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))))
10 oveq2 7416 . . . . 5 (๐‘ฅ = ๐ต โ†’ (๐ถ โ†‘o ๐‘ฅ) = (๐ถ โ†‘o ๐ต))
1110eleq2d 2819 . . . 4 (๐‘ฅ = ๐ต โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต)))
1211imbi2d 340 . . 3 (๐‘ฅ = ๐ต โ†’ ((๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต))))
13 eldifi 4126 . . . . . . . 8 (๐ถ โˆˆ (On โˆ– 2o) โ†’ ๐ถ โˆˆ On)
14 oecl 8536 . . . . . . . 8 ((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ On)
1513, 14sylan 580 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ On)
16 om1 8541 . . . . . . 7 ((๐ถ โ†‘o ๐ด) โˆˆ On โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) = (๐ถ โ†‘o ๐ด))
1715, 16syl 17 . . . . . 6 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) = (๐ถ โ†‘o ๐ด))
18 ondif2 8501 . . . . . . . . 9 (๐ถ โˆˆ (On โˆ– 2o) โ†” (๐ถ โˆˆ On โˆง 1o โˆˆ ๐ถ))
1918simprbi 497 . . . . . . . 8 (๐ถ โˆˆ (On โˆ– 2o) โ†’ 1o โˆˆ ๐ถ)
2019adantr 481 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ 1o โˆˆ ๐ถ)
2113adantr 481 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ๐ถ โˆˆ On)
22 simpr 485 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ๐ด โˆˆ On)
23 dif20el 8504 . . . . . . . . . 10 (๐ถ โˆˆ (On โˆ– 2o) โ†’ โˆ… โˆˆ ๐ถ)
2423adantr 481 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ โˆ… โˆˆ ๐ถ)
25 oen0 8585 . . . . . . . . 9 (((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ถ) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐ด))
2621, 22, 24, 25syl21anc 836 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐ด))
27 omordi 8565 . . . . . . . 8 (((๐ถ โˆˆ On โˆง (๐ถ โ†‘o ๐ด) โˆˆ On) โˆง โˆ… โˆˆ (๐ถ โ†‘o ๐ด)) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ)))
2821, 15, 26, 27syl21anc 836 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ)))
2920, 28mpd 15 . . . . . 6 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ ((๐ถ โ†‘o ๐ด) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
3017, 29eqeltrrd 2834 . . . . 5 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
31 oesuc 8526 . . . . . 6 ((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐ด) = ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
3213, 31sylan 580 . . . . 5 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐ด) = ((๐ถ โ†‘o ๐ด) ยทo ๐ถ))
3330, 32eleqtrrd 2836 . . . 4 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐ด โˆˆ On) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))
3433expcom 414 . . 3 (๐ด โˆˆ On โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
35 oecl 8536 . . . . . . . . . . 11 ((๐ถ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ On)
3613, 35sylan 580 . . . . . . . . . 10 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ On)
37 om1 8541 . . . . . . . . . 10 ((๐ถ โ†‘o ๐‘ฆ) โˆˆ On โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) = (๐ถ โ†‘o ๐‘ฆ))
3836, 37syl 17 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) = (๐ถ โ†‘o ๐‘ฆ))
3919adantr 481 . . . . . . . . . 10 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ 1o โˆˆ ๐ถ)
4013adantr 481 . . . . . . . . . . 11 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ๐ถ โˆˆ On)
41 simpr 485 . . . . . . . . . . . 12 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ๐‘ฆ โˆˆ On)
4223adantr 481 . . . . . . . . . . . 12 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ โˆ… โˆˆ ๐ถ)
43 oen0 8585 . . . . . . . . . . . 12 (((๐ถ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โˆง โˆ… โˆˆ ๐ถ) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐‘ฆ))
4440, 41, 42, 43syl21anc 836 . . . . . . . . . . 11 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ โˆ… โˆˆ (๐ถ โ†‘o ๐‘ฆ))
45 omordi 8565 . . . . . . . . . . 11 (((๐ถ โˆˆ On โˆง (๐ถ โ†‘o ๐‘ฆ) โˆˆ On) โˆง โˆ… โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ)))
4640, 36, 44, 45syl21anc 836 . . . . . . . . . 10 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (1o โˆˆ ๐ถ โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ)))
4739, 46mpd 15 . . . . . . . . 9 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ถ โ†‘o ๐‘ฆ) ยทo 1o) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
4838, 47eqeltrrd 2834 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
49 oesuc 8526 . . . . . . . . 9 ((๐ถ โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) = ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
5013, 49sylan 580 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) = ((๐ถ โ†‘o ๐‘ฆ) ยทo ๐ถ))
5148, 50eleqtrrd 2836 . . . . . . 7 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o ๐‘ฆ) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))
52 onsuc 7798 . . . . . . . . 9 (๐‘ฆ โˆˆ On โ†’ suc ๐‘ฆ โˆˆ On)
53 oecl 8536 . . . . . . . . 9 ((๐ถ โˆˆ On โˆง suc ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) โˆˆ On)
5413, 52, 53syl2an 596 . . . . . . . 8 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ถ โ†‘o suc ๐‘ฆ) โˆˆ On)
55 ontr1 6410 . . . . . . . 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 692 . . . . . 6 ((๐ถ โˆˆ (On โˆ– 2o) โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ)))
5857expcom 414 . . . . 5 (๐‘ฆ โˆˆ On โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐‘ฆ))))
5958adantr 481 . . . 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 388 . . . . . 6 ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
6261ralbii 3093 . . . . 5 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
63 r19.21v 3179 . . . . 5 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
6462, 63bitri 274 . . . 4 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))) โ†” (๐ถ โˆˆ (On โˆ– 2o) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ))))
65 limsuc 7837 . . . . . . . . . 10 (Lim ๐‘ฅ โ†’ (๐ด โˆˆ ๐‘ฅ โ†” suc ๐ด โˆˆ ๐‘ฅ))
6665biimpa 477 . . . . . . . . 9 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โ†’ suc ๐ด โˆˆ ๐‘ฅ)
67 elex 3492 . . . . . . . . . . . . 13 (suc ๐ด โˆˆ ๐‘ฅ โ†’ suc ๐ด โˆˆ V)
68 sucexb 7791 . . . . . . . . . . . . . 14 (๐ด โˆˆ V โ†” suc ๐ด โˆˆ V)
69 sucidg 6445 . . . . . . . . . . . . . 14 (๐ด โˆˆ V โ†’ ๐ด โˆˆ suc ๐ด)
7068, 69sylbir 234 . . . . . . . . . . . . 13 (suc ๐ด โˆˆ V โ†’ ๐ด โˆˆ suc ๐ด)
7167, 70syl 17 . . . . . . . . . . . 12 (suc ๐ด โˆˆ ๐‘ฅ โ†’ ๐ด โˆˆ suc ๐ด)
72 eleq2 2822 . . . . . . . . . . . . . 14 (๐‘ฆ = suc ๐ด โ†’ (๐ด โˆˆ ๐‘ฆ โ†” ๐ด โˆˆ suc ๐ด))
73 oveq2 7416 . . . . . . . . . . . . . . 15 (๐‘ฆ = suc ๐ด โ†’ (๐ถ โ†‘o ๐‘ฆ) = (๐ถ โ†‘o suc ๐ด))
7473eleq2d 2819 . . . . . . . . . . . . . 14 (๐‘ฆ = suc ๐ด โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
7572, 74imbi12d 344 . . . . . . . . . . . . 13 (๐‘ฆ = suc ๐ด โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†” (๐ด โˆˆ suc ๐ด โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
7675rspcv 3608 . . . . . . . . . . . 12 (suc ๐ด โˆˆ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐ด โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
7771, 76mpid 44 . . . . . . . . . . 11 (suc ๐ด โˆˆ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด)))
7877anc2li 556 . . . . . . . . . 10 (suc ๐ด โˆˆ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (suc ๐ด โˆˆ ๐‘ฅ โˆง (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o suc ๐ด))))
7973eliuni 5003 . . . . . . . . . 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 481 . . . . . . 7 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ)))
8313adantl 482 . . . . . . . . . 10 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ ๐ถ โˆˆ On)
84 simpl 483 . . . . . . . . . 10 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ Lim ๐‘ฅ)
8523adantl 482 . . . . . . . . . 10 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ โˆ… โˆˆ ๐ถ)
86 vex 3478 . . . . . . . . . . 11 ๐‘ฅ โˆˆ V
87 oelim 8533 . . . . . . . . . . 11 (((๐ถ โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
8886, 87mpanlr1 704 . . . . . . . . . 10 (((๐ถ โˆˆ On โˆง Lim ๐‘ฅ) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
8983, 84, 85, 88syl21anc 836 . . . . . . . . 9 ((Lim ๐‘ฅ โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
9089adantlr 713 . . . . . . . 8 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (๐ถ โ†‘o ๐‘ฅ) = โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ))
9190eleq2d 2819 . . . . . . 7 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ ((๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ) โ†” (๐ถ โ†‘o ๐ด) โˆˆ โˆช ๐‘ฆ โˆˆ ๐‘ฅ (๐ถ โ†‘o ๐‘ฆ)))
9282, 91sylibrd 258 . . . . . 6 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ ๐‘ฅ) โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฆ)) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐‘ฅ)))
9392ex 413 . . . . 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 7850 . 2 ((๐ต โˆˆ On โˆง ๐ด โˆˆ ๐ต) โ†’ (๐ถ โˆˆ (On โˆ– 2o) โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต)))
9796impancom 452 1 ((๐ต โˆˆ On โˆง ๐ถ โˆˆ (On โˆ– 2o)) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ โ†‘o ๐ด) โˆˆ (๐ถ โ†‘o ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061  Vcvv 3474   โˆ– cdif 3945  โˆ…c0 4322  โˆช ciun 4997  Oncon0 6364  Lim wlim 6365  suc csuc 6366  (class class class)co 7408  1oc1o 8458  2oc2o 8459   ยทo comu 8463   โ†‘o coe 8464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-2o 8466  df-oadd 8469  df-omul 8470  df-oexp 8471
This theorem is referenced by:  oeord  8587  oecan  8588  oeworde  8592  oelimcl  8599  oeord2lim  42049  oeord2i  42050  omcl2  42073
  Copyright terms: Public domain W3C validator