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

Theorem omeulem1 8582
Description: Lemma for omeu 8585: existence part. (Contributed by Mario Carneiro, 28-Feb-2013.)
Assertion
Ref Expression
omeulem1 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
Distinct variable groups:   ๐‘ฅ,๐ด,๐‘ฆ   ๐‘ฅ,๐ต,๐‘ฆ

Proof of Theorem omeulem1
Dummy variables ๐‘ค ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1138 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ ๐ต โˆˆ On)
2 onsucb 7805 . . . . . 6 (๐ต โˆˆ On โ†” suc ๐ต โˆˆ On)
31, 2sylib 217 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ suc ๐ต โˆˆ On)
4 simp1 1137 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ ๐ด โˆˆ On)
5 on0eln0 6421 . . . . . . 7 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
65biimpar 479 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆ… โˆˆ ๐ด)
763adant2 1132 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆ… โˆˆ ๐ด)
8 omword2 8574 . . . . 5 (((suc ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ suc ๐ต โŠ† (๐ด ยทo suc ๐ต))
93, 4, 7, 8syl21anc 837 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ suc ๐ต โŠ† (๐ด ยทo suc ๐ต))
10 sucidg 6446 . . . . 5 (๐ต โˆˆ On โ†’ ๐ต โˆˆ suc ๐ต)
11 ssel 3976 . . . . 5 (suc ๐ต โŠ† (๐ด ยทo suc ๐ต) โ†’ (๐ต โˆˆ suc ๐ต โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐ต)))
1210, 11syl5 34 . . . 4 (suc ๐ต โŠ† (๐ด ยทo suc ๐ต) โ†’ (๐ต โˆˆ On โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐ต)))
139, 1, 12sylc 65 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐ต))
14 suceq 6431 . . . . . 6 (๐‘ฅ = ๐ต โ†’ suc ๐‘ฅ = suc ๐ต)
1514oveq2d 7425 . . . . 5 (๐‘ฅ = ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) = (๐ด ยทo suc ๐ต))
1615eleq2d 2820 . . . 4 (๐‘ฅ = ๐ต โ†’ (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐ต)))
1716rspcev 3613 . . 3 ((๐ต โˆˆ On โˆง ๐ต โˆˆ (๐ด ยทo suc ๐ต)) โ†’ โˆƒ๐‘ฅ โˆˆ On ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ))
181, 13, 17syl2anc 585 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฅ โˆˆ On ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ))
19 suceq 6431 . . . . . 6 (๐‘ฅ = ๐‘ง โ†’ suc ๐‘ฅ = suc ๐‘ง)
2019oveq2d 7425 . . . . 5 (๐‘ฅ = ๐‘ง โ†’ (๐ด ยทo suc ๐‘ฅ) = (๐ด ยทo suc ๐‘ง))
2120eleq2d 2820 . . . 4 (๐‘ฅ = ๐‘ง โ†’ (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
2221onminex 7790 . . 3 (โˆƒ๐‘ฅ โˆˆ On ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ โˆƒ๐‘ฅ โˆˆ On (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
23 vex 3479 . . . . . . . . . . . . . . 15 ๐‘ฅ โˆˆ V
2423elon 6374 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ On โ†” Ord ๐‘ฅ)
25 ordzsl 7834 . . . . . . . . . . . . . 14 (Ord ๐‘ฅ โ†” (๐‘ฅ = โˆ… โˆจ โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โˆจ Lim ๐‘ฅ))
2624, 25bitri 275 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ On โ†” (๐‘ฅ = โˆ… โˆจ โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โˆจ Lim ๐‘ฅ))
27 oveq2 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = โˆ… โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo โˆ…))
28 om0 8517 . . . . . . . . . . . . . . . . . . . 20 (๐ด โˆˆ On โ†’ (๐ด ยทo โˆ…) = โˆ…)
2927, 28sylan9eqr 2795 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ On โˆง ๐‘ฅ = โˆ…) โ†’ (๐ด ยทo ๐‘ฅ) = โˆ…)
30 ne0i 4335 . . . . . . . . . . . . . . . . . . . 20 (๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ (๐ด ยทo ๐‘ฅ) โ‰  โˆ…)
3130necon2bi 2972 . . . . . . . . . . . . . . . . . . 19 ((๐ด ยทo ๐‘ฅ) = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
3229, 31syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ On โˆง ๐‘ฅ = โˆ…) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
3332ex 414 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ On โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
3433a1d 25 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ On โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))))
35343ad2ant1 1134 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))))
3635imp 408 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
37 simp3 1139 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ ๐‘ฅ = suc ๐‘ค)
38 simp2 1138 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง))
39 raleq 3323 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = suc ๐‘ค โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” โˆ€๐‘ง โˆˆ suc ๐‘ค ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
40 vex 3479 . . . . . . . . . . . . . . . . . . . . 21 ๐‘ค โˆˆ V
4140sucid 6447 . . . . . . . . . . . . . . . . . . . 20 ๐‘ค โˆˆ suc ๐‘ค
42 suceq 6431 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ง = ๐‘ค โ†’ suc ๐‘ง = suc ๐‘ค)
4342oveq2d 7425 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ง = ๐‘ค โ†’ (๐ด ยทo suc ๐‘ง) = (๐ด ยทo suc ๐‘ค))
4443eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ง = ๐‘ค โ†’ (๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4544notbid 318 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ง = ๐‘ค โ†’ (ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4645rspcv 3609 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค โˆˆ suc ๐‘ค โ†’ (โˆ€๐‘ง โˆˆ suc ๐‘ค ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4741, 46ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (โˆ€๐‘ง โˆˆ suc ๐‘ค ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค))
4839, 47syl6bi 253 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = suc ๐‘ค โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4937, 38, 48sylc 65 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค))
50 oveq2 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = suc ๐‘ค โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo suc ๐‘ค))
5150eleq2d 2820 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = suc ๐‘ค โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
5251notbid 318 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = suc ๐‘ค โ†’ (ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†” ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
5352biimpar 479 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ = suc ๐‘ค โˆง ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
5437, 49, 53syl2anc 585 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
55543expia 1122 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ = suc ๐‘ค โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
5655rexlimdvw 3161 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
57 ralnex 3073 . . . . . . . . . . . . . . . . . 18 (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” ยฌ โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง))
58 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ ๐ด โˆˆ On)
5923a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ ๐‘ฅ โˆˆ V)
60 simpl 484 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ Lim ๐‘ฅ)
61 omlim 8533 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โ†’ (๐ด ยทo ๐‘ฅ) = โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง))
6258, 59, 60, 61syl12anc 836 . . . . . . . . . . . . . . . . . . . . 21 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) = โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง))
6362eleq2d 2820 . . . . . . . . . . . . . . . . . . . 20 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†” ๐ต โˆˆ โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง)))
64 eliun 5002 . . . . . . . . . . . . . . . . . . . . 21 (๐ต โˆˆ โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โ†” โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo ๐‘ง))
65 limord 6425 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim ๐‘ฅ โ†’ Ord ๐‘ฅ)
66653ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ Ord ๐‘ฅ)
6766, 24sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ On)
68 simp3 1139 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ง โˆˆ ๐‘ฅ)
69 onelon 6390 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฅ โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ง โˆˆ On)
7067, 68, 69syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ง โˆˆ On)
71 onsuc 7799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ง โˆˆ On โ†’ suc ๐‘ง โˆˆ On)
7270, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ suc ๐‘ง โˆˆ On)
73 simp2 1138 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐ด โˆˆ On)
74 sssucid 6445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ๐‘ง โŠ† suc ๐‘ง
75 omwordi 8571 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ง โˆˆ On โˆง suc ๐‘ง โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โŠ† suc ๐‘ง โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo suc ๐‘ง)))
7674, 75mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ง โˆˆ On โˆง suc ๐‘ง โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo suc ๐‘ง))
7770, 72, 73, 76syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo suc ๐‘ง))
7877sseld 3982 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ง) โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
79783expia 1122 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โˆˆ ๐‘ฅ โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ง) โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง))))
8079reximdvai 3166 . . . . . . . . . . . . . . . . . . . . 21 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo ๐‘ง) โ†’ โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
8164, 80biimtrid 241 . . . . . . . . . . . . . . . . . . . 20 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐ต โˆˆ โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โ†’ โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
8263, 81sylbid 239 . . . . . . . . . . . . . . . . . . 19 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
8382con3d 152 . . . . . . . . . . . . . . . . . 18 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (ยฌ โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8457, 83biimtrid 241 . . . . . . . . . . . . . . . . 17 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8584expimpd 455 . . . . . . . . . . . . . . . 16 (Lim ๐‘ฅ โ†’ ((๐ด โˆˆ On โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8685com12 32 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (Lim ๐‘ฅ โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
87863ad2antl1 1186 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (Lim ๐‘ฅ โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8836, 56, 873jaod 1429 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ ((๐‘ฅ = โˆ… โˆจ โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โˆจ Lim ๐‘ฅ) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8926, 88biimtrid 241 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
9089impr 456 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
91 simpl1 1192 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ๐ด โˆˆ On)
92 simprr 772 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ๐‘ฅ โˆˆ On)
93 omcl 8536 . . . . . . . . . . . . 13 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
9491, 92, 93syl2anc 585 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
95 simpl2 1193 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ๐ต โˆˆ On)
96 ontri1 6399 . . . . . . . . . . . 12 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
9794, 95, 96syl2anc 585 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
9890, 97mpbird 257 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ (๐ด ยทo ๐‘ฅ) โŠ† ๐ต)
99 oawordex 8557 . . . . . . . . . . 11 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
10094, 95, 99syl2anc 585 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
10198, 100mpbid 231 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
1021013adantr1 1170 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
103 simp3r 1203 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
104 simp21 1207 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ))
105 simp11 1204 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐ด โˆˆ On)
106 simp23 1209 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐‘ฅ โˆˆ On)
107 omsuc 8526 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
108105, 106, 107syl2anc 585 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
109104, 108eleqtrd 2836 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐ต โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด))
110103, 109eqeltrd 2834 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด))
111 simp3l 1202 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐‘ฆ โˆˆ On)
112105, 106, 93syl2anc 585 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
113 oaord 8547 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
114111, 105, 112, 113syl3anc 1372 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
115110, 114mpbird 257 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐‘ฆ โˆˆ ๐ด)
116115, 103jca 513 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐‘ฆ โˆˆ ๐ด โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
1171163expia 1122 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต) โ†’ (๐‘ฆ โˆˆ ๐ด โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)))
118117reximdv2 3165 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ (โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
119102, 118mpd 15 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
120119expcom 415 . . . . . 6 ((๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
1211203expia 1122 . . . . 5 ((๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ โˆˆ On โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)))
122121com13 88 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ (๐‘ฅ โˆˆ On โ†’ ((๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)))
123122reximdvai 3166 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ (โˆƒ๐‘ฅ โˆˆ On (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
12422, 123syl5 34 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ (โˆƒ๐‘ฅ โˆˆ On ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
12518, 124mpd 15 1 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ w3o 1087   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  โˆ€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:  omeu  8585  dflim5  42079
  Copyright terms: Public domain W3C validator