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

Theorem omeulem1 8584
Description: Lemma for omeu 8587: 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 1137 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ ๐ต โˆˆ On)
2 onsucb 7807 . . . . . 6 (๐ต โˆˆ On โ†” suc ๐ต โˆˆ On)
31, 2sylib 217 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ suc ๐ต โˆˆ On)
4 simp1 1136 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ ๐ด โˆˆ On)
5 on0eln0 6420 . . . . . . 7 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
65biimpar 478 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆ… โˆˆ ๐ด)
763adant2 1131 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆ… โˆˆ ๐ด)
8 omword2 8576 . . . . 5 (((suc ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ suc ๐ต โŠ† (๐ด ยทo suc ๐ต))
93, 4, 7, 8syl21anc 836 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ suc ๐ต โŠ† (๐ด ยทo suc ๐ต))
10 sucidg 6445 . . . . 5 (๐ต โˆˆ On โ†’ ๐ต โˆˆ suc ๐ต)
11 ssel 3975 . . . . 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 6430 . . . . . 6 (๐‘ฅ = ๐ต โ†’ suc ๐‘ฅ = suc ๐ต)
1514oveq2d 7427 . . . . 5 (๐‘ฅ = ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) = (๐ด ยทo suc ๐ต))
1615eleq2d 2819 . . . 4 (๐‘ฅ = ๐ต โ†’ (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐ต)))
1716rspcev 3612 . . 3 ((๐ต โˆˆ On โˆง ๐ต โˆˆ (๐ด ยทo suc ๐ต)) โ†’ โˆƒ๐‘ฅ โˆˆ On ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ))
181, 13, 17syl2anc 584 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฅ โˆˆ On ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ))
19 suceq 6430 . . . . . 6 (๐‘ฅ = ๐‘ง โ†’ suc ๐‘ฅ = suc ๐‘ง)
2019oveq2d 7427 . . . . 5 (๐‘ฅ = ๐‘ง โ†’ (๐ด ยทo suc ๐‘ฅ) = (๐ด ยทo suc ๐‘ง))
2120eleq2d 2819 . . . 4 (๐‘ฅ = ๐‘ง โ†’ (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
2221onminex 7792 . . 3 (โˆƒ๐‘ฅ โˆˆ On ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โ†’ โˆƒ๐‘ฅ โˆˆ On (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
23 vex 3478 . . . . . . . . . . . . . . 15 ๐‘ฅ โˆˆ V
2423elon 6373 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ On โ†” Ord ๐‘ฅ)
25 ordzsl 7836 . . . . . . . . . . . . . 14 (Ord ๐‘ฅ โ†” (๐‘ฅ = โˆ… โˆจ โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โˆจ Lim ๐‘ฅ))
2624, 25bitri 274 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ On โ†” (๐‘ฅ = โˆ… โˆจ โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โˆจ Lim ๐‘ฅ))
27 oveq2 7419 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = โˆ… โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo โˆ…))
28 om0 8519 . . . . . . . . . . . . . . . . . . . 20 (๐ด โˆˆ On โ†’ (๐ด ยทo โˆ…) = โˆ…)
2927, 28sylan9eqr 2794 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ On โˆง ๐‘ฅ = โˆ…) โ†’ (๐ด ยทo ๐‘ฅ) = โˆ…)
30 ne0i 4334 . . . . . . . . . . . . . . . . . . . 20 (๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†’ (๐ด ยทo ๐‘ฅ) โ‰  โˆ…)
3130necon2bi 2971 . . . . . . . . . . . . . . . . . . 19 ((๐ด ยทo ๐‘ฅ) = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
3229, 31syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ On โˆง ๐‘ฅ = โˆ…) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
3332ex 413 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ On โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
3433a1d 25 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ On โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))))
35343ad2ant1 1133 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))))
3635imp 407 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ = โˆ… โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
37 simp3 1138 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ ๐‘ฅ = suc ๐‘ค)
38 simp2 1137 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง))
39 raleq 3322 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = suc ๐‘ค โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” โˆ€๐‘ง โˆˆ suc ๐‘ค ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
40 vex 3478 . . . . . . . . . . . . . . . . . . . . 21 ๐‘ค โˆˆ V
4140sucid 6446 . . . . . . . . . . . . . . . . . . . 20 ๐‘ค โˆˆ suc ๐‘ค
42 suceq 6430 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ง = ๐‘ค โ†’ suc ๐‘ง = suc ๐‘ค)
4342oveq2d 7427 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ง = ๐‘ค โ†’ (๐ด ยทo suc ๐‘ง) = (๐ด ยทo suc ๐‘ค))
4443eleq2d 2819 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ง = ๐‘ค โ†’ (๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4544notbid 317 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ง = ๐‘ค โ†’ (ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4645rspcv 3608 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค โˆˆ suc ๐‘ค โ†’ (โˆ€๐‘ง โˆˆ suc ๐‘ค ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4741, 46ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (โˆ€๐‘ง โˆˆ suc ๐‘ค ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค))
4839, 47syl6bi 252 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = suc ๐‘ค โ†’ (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
4937, 38, 48sylc 65 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค))
50 oveq2 7419 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = suc ๐‘ค โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo suc ๐‘ค))
5150eleq2d 2819 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = suc ๐‘ค โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†” ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
5251notbid 317 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = suc ๐‘ค โ†’ (ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†” ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)))
5352biimpar 478 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ = suc ๐‘ค โˆง ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ค)) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
5437, 49, 53syl2anc 584 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ = suc ๐‘ค) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
55543expia 1121 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ = suc ๐‘ค โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
5655rexlimdvw 3160 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
57 ralnex 3072 . . . . . . . . . . . . . . . . . 18 (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โ†” ยฌ โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง))
58 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ ๐ด โˆˆ On)
5923a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ ๐‘ฅ โˆˆ V)
60 simpl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ Lim ๐‘ฅ)
61 omlim 8535 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โ†’ (๐ด ยทo ๐‘ฅ) = โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง))
6258, 59, 60, 61syl12anc 835 . . . . . . . . . . . . . . . . . . . . 21 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) = โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง))
6362eleq2d 2819 . . . . . . . . . . . . . . . . . . . 20 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ฅ) โ†” ๐ต โˆˆ โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง)))
64 eliun 5001 . . . . . . . . . . . . . . . . . . . . 21 (๐ต โˆˆ โˆช ๐‘ง โˆˆ ๐‘ฅ (๐ด ยทo ๐‘ง) โ†” โˆƒ๐‘ง โˆˆ ๐‘ฅ ๐ต โˆˆ (๐ด ยทo ๐‘ง))
65 limord 6424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim ๐‘ฅ โ†’ Ord ๐‘ฅ)
66653ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ Ord ๐‘ฅ)
6766, 24sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ On)
68 simp3 1138 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ง โˆˆ ๐‘ฅ)
69 onelon 6389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฅ โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ง โˆˆ On)
7067, 68, 69syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐‘ง โˆˆ On)
71 onsuc 7801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ง โˆˆ On โ†’ suc ๐‘ง โˆˆ On)
7270, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ suc ๐‘ง โˆˆ On)
73 simp2 1137 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ ๐ด โˆˆ On)
74 sssucid 6444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ๐‘ง โŠ† suc ๐‘ง
75 omwordi 8573 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ง โˆˆ On โˆง suc ๐‘ง โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โŠ† suc ๐‘ง โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo suc ๐‘ง)))
7674, 75mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ง โˆˆ On โˆง suc ๐‘ง โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo suc ๐‘ง))
7770, 72, 73, 76syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo suc ๐‘ง))
7877sseld 3981 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On โˆง ๐‘ง โˆˆ ๐‘ฅ) โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ง) โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)))
79783expia 1121 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โ†’ (๐‘ง โˆˆ ๐‘ฅ โ†’ (๐ต โˆˆ (๐ด ยทo ๐‘ง) โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง))))
8079reximdvai 3165 . . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . 16 (Lim ๐‘ฅ โ†’ ((๐ด โˆˆ On โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8685com12 32 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (Lim ๐‘ฅ โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
87863ad2antl1 1185 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (Lim ๐‘ฅ โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8836, 56, 873jaod 1428 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ ((๐‘ฅ = โˆ… โˆจ โˆƒ๐‘ค โˆˆ On ๐‘ฅ = suc ๐‘ค โˆจ Lim ๐‘ฅ) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
8926, 88biimtrid 241 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ โˆˆ On โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
9089impr 455 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ))
91 simpl1 1191 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ๐ด โˆˆ On)
92 simprr 771 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ๐‘ฅ โˆˆ On)
93 omcl 8538 . . . . . . . . . . . . 13 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
9491, 92, 93syl2anc 584 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
95 simpl2 1192 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ๐ต โˆˆ On)
96 ontri1 6398 . . . . . . . . . . . 12 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
9794, 95, 96syl2anc 584 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” ยฌ ๐ต โˆˆ (๐ด ยทo ๐‘ฅ)))
9890, 97mpbird 256 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ (๐ด ยทo ๐‘ฅ) โŠ† ๐ต)
99 oawordex 8559 . . . . . . . . . . 11 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
10094, 95, 99syl2anc 584 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐ด ยทo ๐‘ฅ) โŠ† ๐ต โ†” โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
10198, 100mpbid 231 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
1021013adantr1 1169 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ โˆƒ๐‘ฆ โˆˆ On ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
103 simp3r 1202 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)
104 simp21 1206 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ))
105 simp11 1203 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐ด โˆˆ On)
106 simp23 1208 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐‘ฅ โˆˆ On)
107 omsuc 8528 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
108105, 106, 107syl2anc 584 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
109104, 108eleqtrd 2835 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐ต โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด))
110103, 109eqeltrd 2833 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด))
111 simp3l 1201 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐‘ฆ โˆˆ On)
112105, 106, 93syl2anc 584 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
113 oaord 8549 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
114111, 105, 112, 113syl3anc 1371 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
115110, 114mpbird 256 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ ๐‘ฆ โˆˆ ๐ด)
116115, 103jca 512 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โˆง (๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)) โ†’ (๐‘ฆ โˆˆ ๐ด โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
1171163expia 1121 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โˆง (๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On)) โ†’ ((๐‘ฆ โˆˆ On โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต) โ†’ (๐‘ฆ โˆˆ ๐ด โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)))
118117reximdv2 3164 . . . . . . . 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 414 . . . . . 6 ((๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง) โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต))
1211203expia 1121 . . . . 5 ((๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ (๐‘ฅ โˆˆ On โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)))
122121com13 88 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ (๐‘ฅ โˆˆ On โ†’ ((๐ต โˆˆ (๐ด ยทo suc ๐‘ฅ) โˆง โˆ€๐‘ง โˆˆ ๐‘ฅ ยฌ ๐ต โˆˆ (๐ด ยทo suc ๐‘ง)) โ†’ โˆƒ๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐ต)))
123122reximdvai 3165 . . 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 396   โˆจ w3o 1086   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070  Vcvv 3474   โŠ† wss 3948  โˆ…c0 4322  โˆช ciun 4997  Ord word 6363  Oncon0 6364  Lim wlim 6365  suc csuc 6366  (class class class)co 7411   +o coa 8465   ยทo comu 8466
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 7727
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-rmo 3376  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-int 4951  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 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-omul 8473
This theorem is referenced by:  omeu  8587  dflim5  42161
  Copyright terms: Public domain W3C validator