Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  omcl2 Structured version   Visualization version   GIF version

Theorem omcl2 42762
Description: Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.)
Assertion
Ref Expression
omcl2 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = โˆ… โˆจ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On))) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)

Proof of Theorem omcl2
Dummy variable ๐‘ฅ is distinct from all other variables.
StepHypRef Expression
1 eleq2 2818 . . . . . 6 (๐ถ = โˆ… โ†’ (๐ด โˆˆ ๐ถ โ†” ๐ด โˆˆ โˆ…))
2 noel 4331 . . . . . . 7 ยฌ ๐ด โˆˆ โˆ…
32pm2.21i 119 . . . . . 6 (๐ด โˆˆ โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
41, 3biimtrdi 252 . . . . 5 (๐ถ = โˆ… โ†’ (๐ด โˆˆ ๐ถ โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
54com12 32 . . . 4 (๐ด โˆˆ ๐ถ โ†’ (๐ถ = โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
65adantr 480 . . 3 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ (๐ถ = โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
7 simpl 482 . . . . . . . 8 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
8 omelon 9670 . . . . . . . . . . . 12 ฯ‰ โˆˆ On
9 oecl 8558 . . . . . . . . . . . 12 ((ฯ‰ โˆˆ On โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ท) โˆˆ On)
108, 9mpan 689 . . . . . . . . . . 11 (๐ท โˆˆ On โ†’ (ฯ‰ โ†‘o ๐ท) โˆˆ On)
1110, 8jctil 519 . . . . . . . . . 10 (๐ท โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ท) โˆˆ On))
12 oecl 8558 . . . . . . . . . 10 ((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ท) โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆˆ On)
1311, 12syl 17 . . . . . . . . 9 (๐ท โˆˆ On โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆˆ On)
1413adantl 481 . . . . . . . 8 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆˆ On)
157, 14eqeltrd 2829 . . . . . . 7 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ โˆˆ On)
16 simpll 766 . . . . . . 7 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ด โˆˆ ๐ถ)
17 onelon 6394 . . . . . . 7 ((๐ถ โˆˆ On โˆง ๐ด โˆˆ ๐ถ) โ†’ ๐ด โˆˆ On)
1815, 16, 17syl2an2 685 . . . . . 6 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ด โˆˆ On)
19 on0eqel 6493 . . . . . 6 (๐ด โˆˆ On โ†’ (๐ด = โˆ… โˆจ โˆ… โˆˆ ๐ด))
2018, 19syl 17 . . . . 5 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด = โˆ… โˆจ โˆ… โˆˆ ๐ด))
21 oveq1 7427 . . . . . . . . 9 (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) = (โˆ… ยทo ๐ต))
22 simpr 484 . . . . . . . . . . . 12 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ ๐ต โˆˆ ๐ถ)
2322adantr 480 . . . . . . . . . . 11 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ ๐ถ)
24 onelon 6394 . . . . . . . . . . 11 ((๐ถ โˆˆ On โˆง ๐ต โˆˆ ๐ถ) โ†’ ๐ต โˆˆ On)
2515, 23, 24syl2an2 685 . . . . . . . . . 10 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ On)
26 om0r 8560 . . . . . . . . . 10 (๐ต โˆˆ On โ†’ (โˆ… ยทo ๐ต) = โˆ…)
2725, 26syl 17 . . . . . . . . 9 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (โˆ… ยทo ๐ต) = โˆ…)
2821, 27sylan9eqr 2790 . . . . . . . 8 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ด = โˆ…) โ†’ (๐ด ยทo ๐ต) = โˆ…)
29 peano1 7894 . . . . . . . . . . . . 13 โˆ… โˆˆ ฯ‰
30 oen0 8607 . . . . . . . . . . . . 13 (((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ท) โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
3111, 29, 30sylancl 585 . . . . . . . . . . . 12 (๐ท โˆˆ On โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
3231adantl 481 . . . . . . . . . . 11 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
3332, 7eleqtrrd 2832 . . . . . . . . . 10 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆ… โˆˆ ๐ถ)
3433adantl 481 . . . . . . . . 9 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ โˆ… โˆˆ ๐ถ)
3534adantr 480 . . . . . . . 8 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ด = โˆ…) โ†’ โˆ… โˆˆ ๐ถ)
3628, 35eqeltrd 2829 . . . . . . 7 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ด = โˆ…) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
3736ex 412 . . . . . 6 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
38 simp1 1134 . . . . . . . . . . . 12 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โ†’ ๐ด โˆˆ ๐ถ)
3915adantl 481 . . . . . . . . . . . . . 14 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ถ โˆˆ On)
40 simpr 484 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ถ โˆˆ On) โ†’ ๐ถ โˆˆ On)
4138ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ถ โˆˆ On) โ†’ ๐ด โˆˆ ๐ถ)
4240, 41, 17syl2anc 583 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ถ โˆˆ On) โ†’ ๐ด โˆˆ On)
4342ex 412 . . . . . . . . . . . . . 14 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ถ โˆˆ On โ†’ ๐ด โˆˆ On))
4439, 43jcai 516 . . . . . . . . . . . . 13 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ถ โˆˆ On โˆง ๐ด โˆˆ On))
45 simpl3 1191 . . . . . . . . . . . . 13 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ โˆ… โˆˆ ๐ด)
46 simpl2 1190 . . . . . . . . . . . . 13 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ ๐ถ)
47 omordi 8587 . . . . . . . . . . . . . 14 (((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ต โˆˆ ๐ถ โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ)))
4847imp 406 . . . . . . . . . . . . 13 ((((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โˆง ๐ต โˆˆ ๐ถ) โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ))
4944, 45, 46, 48syl21anc 837 . . . . . . . . . . . 12 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ))
50 oveq1 7427 . . . . . . . . . . . . 13 (๐‘ฅ = ๐ด โ†’ (๐‘ฅ ยทo ๐ถ) = (๐ด ยทo ๐ถ))
5150eliuni 5002 . . . . . . . . . . . 12 ((๐ด โˆˆ ๐ถ โˆง (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ)) โ†’ (๐ด ยทo ๐ต) โˆˆ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
5238, 49, 51syl2an2r 684 . . . . . . . . . . 11 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
53 simpr 484 . . . . . . . . . . . . . . . . . 18 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฅ = โˆ…)
5453oveq1d 7435 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฅ ยทo ๐ถ) = (โˆ… ยทo ๐ถ))
55 om0r 8560 . . . . . . . . . . . . . . . . . . 19 (๐ถ โˆˆ On โ†’ (โˆ… ยทo ๐ถ) = โˆ…)
5615, 55syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (โˆ… ยทo ๐ถ) = โˆ…)
5756ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (โˆ… ยทo ๐ถ) = โˆ…)
5854, 57eqtrd 2768 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฅ ยทo ๐ถ) = โˆ…)
59 0ss 4397 . . . . . . . . . . . . . . . . 17 โˆ… โІ ๐ถ
6059a1i 11 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ โˆ… โІ ๐ถ)
6158, 60eqsstrd 4018 . . . . . . . . . . . . . . 15 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
62 id 22 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ))
6362adantll 713 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ))
64 simpll 766 . . . . . . . . . . . . . . . . . 18 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On))
65643mix3d 1336 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐ถ = โˆ… โˆจ ๐ถ = 2o โˆจ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)))
66 omabs2 42761 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ) โˆง (๐ถ = โˆ… โˆจ ๐ถ = 2o โˆจ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On))) โ†’ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
6763, 65, 66syl2anc 583 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
68 ssidd 4003 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ๐ถ โІ ๐ถ)
6967, 68eqsstrd 4018 . . . . . . . . . . . . . . 15 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
70 onelon 6394 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ ๐‘ฅ โˆˆ On)
7115, 70sylan 579 . . . . . . . . . . . . . . . 16 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ ๐‘ฅ โˆˆ On)
72 on0eqel 6493 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
7371, 72syl 17 . . . . . . . . . . . . . . 15 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
7461, 69, 73mpjaodan 957 . . . . . . . . . . . . . 14 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
7574iunssd 5053 . . . . . . . . . . . . 13 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
76 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ท โˆˆ On)
7776, 8jctil 519 . . . . . . . . . . . . . . . . . 18 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โˆˆ On โˆง ๐ท โˆˆ On))
78 oen0 8607 . . . . . . . . . . . . . . . . . 18 (((ฯ‰ โˆˆ On โˆง ๐ท โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ท))
7977, 29, 78sylancl 585 . . . . . . . . . . . . . . . . 17 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ท))
8077, 9syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ท) โˆˆ On)
81 1onn 8661 . . . . . . . . . . . . . . . . . . 19 1o โˆˆ ฯ‰
82 ondif2 8523 . . . . . . . . . . . . . . . . . . 19 (ฯ‰ โˆˆ (On โˆ– 2o) โ†” (ฯ‰ โˆˆ On โˆง 1o โˆˆ ฯ‰))
838, 81, 82mpbir2an 710 . . . . . . . . . . . . . . . . . 18 ฯ‰ โˆˆ (On โˆ– 2o)
84 oeordi 8608 . . . . . . . . . . . . . . . . . 18 (((ฯ‰ โ†‘o ๐ท) โˆˆ On โˆง ฯ‰ โˆˆ (On โˆ– 2o)) โ†’ (โˆ… โˆˆ (ฯ‰ โ†‘o ๐ท) โ†’ (ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท))))
8580, 83, 84sylancl 585 . . . . . . . . . . . . . . . . 17 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (โˆ… โˆˆ (ฯ‰ โ†‘o ๐ท) โ†’ (ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท))))
8679, 85mpd 15 . . . . . . . . . . . . . . . 16 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โ†‘o โˆ…) โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
87 oe0 8543 . . . . . . . . . . . . . . . . . . 19 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o โˆ…) = 1o)
888, 87ax-mp 5 . . . . . . . . . . . . . . . . . 18 (ฯ‰ โ†‘o โˆ…) = 1o
8988eqcomi 2737 . . . . . . . . . . . . . . . . 17 1o = (ฯ‰ โ†‘o โˆ…)
9089a1i 11 . . . . . . . . . . . . . . . 16 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ 1o = (ฯ‰ โ†‘o โˆ…))
9186, 90, 73eltr4d 2844 . . . . . . . . . . . . . . 15 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ 1o โˆˆ ๐ถ)
92 oveq1 7427 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = 1o โ†’ (๐‘ฅ ยทo ๐ถ) = (1o ยทo ๐ถ))
93 om1r 8564 . . . . . . . . . . . . . . . . . 18 (๐ถ โˆˆ On โ†’ (1o ยทo ๐ถ) = ๐ถ)
9415, 93syl 17 . . . . . . . . . . . . . . . . 17 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (1o ยทo ๐ถ) = ๐ถ)
9592, 94sylan9eqr 2790 . . . . . . . . . . . . . . . 16 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ = 1o) โ†’ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
9695sseq2d 4012 . . . . . . . . . . . . . . 15 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ = 1o) โ†’ (๐ถ โІ (๐‘ฅ ยทo ๐ถ) โ†” ๐ถ โІ ๐ถ))
97 ssidd 4003 . . . . . . . . . . . . . . 15 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ โІ ๐ถ)
9891, 96, 97rspcedvd 3611 . . . . . . . . . . . . . 14 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ถ ๐ถ โІ (๐‘ฅ ยทo ๐ถ))
99 ssiun 5049 . . . . . . . . . . . . . 14 (โˆƒ๐‘ฅ โˆˆ ๐ถ ๐ถ โІ (๐‘ฅ ยทo ๐ถ) โ†’ ๐ถ โІ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
10098, 99syl 17 . . . . . . . . . . . . 13 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ โІ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
10175, 100eqssd 3997 . . . . . . . . . . . 12 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
102101adantl 481 . . . . . . . . . . 11 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
10352, 102eleqtrd 2831 . . . . . . . . . 10 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
104103ex 412 . . . . . . . . 9 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
1051043expia 1119 . . . . . . . 8 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ (โˆ… โˆˆ ๐ด โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)))
106105com23 86 . . . . . . 7 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)))
107106imp 406 . . . . . 6 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
10837, 107jaod 858 . . . . 5 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ((๐ด = โˆ… โˆจ โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
10920, 108mpd 15 . . . 4 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
110109ex 412 . . 3 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
1116, 110jaod 858 . 2 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ ((๐ถ = โˆ… โˆจ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
112111imp 406 1 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = โˆ… โˆจ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On))) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆจ wo 846   โˆจ w3o 1084   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099  โˆƒwrex 3067   โˆ– cdif 3944   โІ wss 3947  โˆ…c0 4323  โˆช ciun 4996  Oncon0 6369  (class class class)co 7420  ฯ‰com 7870  1oc1o 8480  2oc2o 8481   ยทo comu 8485   โ†‘o coe 8486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5429  ax-un 7740  ax-reg 9616  ax-inf2 9665
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-ot 4638  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-omul 8492  df-oexp 8493
This theorem is referenced by:  omcl3g  42763
  Copyright terms: Public domain W3C validator