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 42633
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 2814 . . . . . 6 (๐ถ = โˆ… โ†’ (๐ด โˆˆ ๐ถ โ†” ๐ด โˆˆ โˆ…))
2 noel 4323 . . . . . . 7 ยฌ ๐ด โˆˆ โˆ…
32pm2.21i 119 . . . . . 6 (๐ด โˆˆ โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
41, 3syl6bi 253 . . . . 5 (๐ถ = โˆ… โ†’ (๐ด โˆˆ ๐ถ โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
54com12 32 . . . 4 (๐ด โˆˆ ๐ถ โ†’ (๐ถ = โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
65adantr 480 . . 3 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ (๐ถ = โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
7 simpl 482 . . . . . . . 8 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
8 omelon 9638 . . . . . . . . . . . 12 ฯ‰ โˆˆ On
9 oecl 8533 . . . . . . . . . . . 12 ((ฯ‰ โˆˆ On โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ท) โˆˆ On)
108, 9mpan 687 . . . . . . . . . . 11 (๐ท โˆˆ On โ†’ (ฯ‰ โ†‘o ๐ท) โˆˆ On)
1110, 8jctil 519 . . . . . . . . . 10 (๐ท โˆˆ On โ†’ (ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ท) โˆˆ On))
12 oecl 8533 . . . . . . . . . 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 2825 . . . . . . 7 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ โˆˆ On)
16 simpll 764 . . . . . . 7 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ด โˆˆ ๐ถ)
17 onelon 6380 . . . . . . 7 ((๐ถ โˆˆ On โˆง ๐ด โˆˆ ๐ถ) โ†’ ๐ด โˆˆ On)
1815, 16, 17syl2an2 683 . . . . . 6 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ด โˆˆ On)
19 on0eqel 6479 . . . . . 6 (๐ด โˆˆ On โ†’ (๐ด = โˆ… โˆจ โˆ… โˆˆ ๐ด))
2018, 19syl 17 . . . . 5 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด = โˆ… โˆจ โˆ… โˆˆ ๐ด))
21 oveq1 7409 . . . . . . . . 9 (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) = (โˆ… ยทo ๐ต))
22 simpr 484 . . . . . . . . . . . 12 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ ๐ต โˆˆ ๐ถ)
2322adantr 480 . . . . . . . . . . 11 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ ๐ถ)
24 onelon 6380 . . . . . . . . . . 11 ((๐ถ โˆˆ On โˆง ๐ต โˆˆ ๐ถ) โ†’ ๐ต โˆˆ On)
2515, 23, 24syl2an2 683 . . . . . . . . . 10 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ On)
26 om0r 8535 . . . . . . . . . 10 (๐ต โˆˆ On โ†’ (โˆ… ยทo ๐ต) = โˆ…)
2725, 26syl 17 . . . . . . . . 9 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (โˆ… ยทo ๐ต) = โˆ…)
2821, 27sylan9eqr 2786 . . . . . . . 8 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ด = โˆ…) โ†’ (๐ด ยทo ๐ต) = โˆ…)
29 peano1 7873 . . . . . . . . . . . . 13 โˆ… โˆˆ ฯ‰
30 oen0 8582 . . . . . . . . . . . . 13 (((ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o ๐ท) โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
3111, 29, 30sylancl 585 . . . . . . . . . . . 12 (๐ท โˆˆ On โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
3231adantl 481 . . . . . . . . . . 11 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)))
3332, 7eleqtrrd 2828 . . . . . . . . . 10 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆ… โˆˆ ๐ถ)
3433adantl 481 . . . . . . . . 9 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ โˆ… โˆˆ ๐ถ)
3534adantr 480 . . . . . . . 8 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ด = โˆ…) โ†’ โˆ… โˆˆ ๐ถ)
3628, 35eqeltrd 2825 . . . . . . 7 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ด = โˆ…) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
3736ex 412 . . . . . 6 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
38 simp1 1133 . . . . . . . . . . . 12 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โ†’ ๐ด โˆˆ ๐ถ)
3915adantl 481 . . . . . . . . . . . . . 14 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ถ โˆˆ On)
40 simpr 484 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โˆง ๐ถ โˆˆ On) โ†’ ๐ถ โˆˆ On)
4138ad2antrr 723 . . . . . . . . . . . . . . . 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 1190 . . . . . . . . . . . . 13 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ โˆ… โˆˆ ๐ด)
46 simpl2 1189 . . . . . . . . . . . . 13 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ๐ต โˆˆ ๐ถ)
47 omordi 8562 . . . . . . . . . . . . . 14 (((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐ต โˆˆ ๐ถ โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ)))
4847imp 406 . . . . . . . . . . . . 13 ((((๐ถ โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โˆง ๐ต โˆˆ ๐ถ) โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ))
4944, 45, 46, 48syl21anc 835 . . . . . . . . . . . 12 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ))
50 oveq1 7409 . . . . . . . . . . . . 13 (๐‘ฅ = ๐ด โ†’ (๐‘ฅ ยทo ๐ถ) = (๐ด ยทo ๐ถ))
5150eliuni 4994 . . . . . . . . . . . 12 ((๐ด โˆˆ ๐ถ โˆง (๐ด ยทo ๐ต) โˆˆ (๐ด ยทo ๐ถ)) โ†’ (๐ด ยทo ๐ต) โˆˆ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
5238, 49, 51syl2an2r 682 . . . . . . . . . . 11 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
53 simpr 484 . . . . . . . . . . . . . . . . . 18 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ ๐‘ฅ = โˆ…)
5453oveq1d 7417 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฅ ยทo ๐ถ) = (โˆ… ยทo ๐ถ))
55 om0r 8535 . . . . . . . . . . . . . . . . . . 19 (๐ถ โˆˆ On โ†’ (โˆ… ยทo ๐ถ) = โˆ…)
5615, 55syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (โˆ… ยทo ๐ถ) = โˆ…)
5756ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (โˆ… ยทo ๐ถ) = โˆ…)
5854, 57eqtrd 2764 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฅ ยทo ๐ถ) = โˆ…)
59 0ss 4389 . . . . . . . . . . . . . . . . 17 โˆ… โІ ๐ถ
6059a1i 11 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ โˆ… โІ ๐ถ)
6158, 60eqsstrd 4013 . . . . . . . . . . . . . . 15 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง ๐‘ฅ = โˆ…) โ†’ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
62 id 22 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ))
6362adantll 711 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ))
64 simpll 764 . . . . . . . . . . . . . . . . . 18 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On))
65643mix3d 1335 . . . . . . . . . . . . . . . . 17 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐ถ = โˆ… โˆจ ๐ถ = 2o โˆจ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)))
66 omabs2 42632 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐‘ฅ) โˆง (๐ถ = โˆ… โˆจ ๐ถ = 2o โˆจ (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On))) โ†’ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
6763, 65, 66syl2anc 583 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
68 ssidd 3998 . . . . . . . . . . . . . . . 16 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ ๐ถ โІ ๐ถ)
6967, 68eqsstrd 4013 . . . . . . . . . . . . . . 15 ((((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โˆง โˆ… โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
70 onelon 6380 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ ๐‘ฅ โˆˆ On)
7115, 70sylan 579 . . . . . . . . . . . . . . . 16 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ ๐‘ฅ โˆˆ On)
72 on0eqel 6479 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
7371, 72syl 17 . . . . . . . . . . . . . . 15 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
7461, 69, 73mpjaodan 955 . . . . . . . . . . . . . 14 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ โˆˆ ๐ถ) โ†’ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
7574iunssd 5044 . . . . . . . . . . . . 13 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ) โІ ๐ถ)
76 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ท โˆˆ On)
7776, 8jctil 519 . . . . . . . . . . . . . . . . . 18 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โˆˆ On โˆง ๐ท โˆˆ On))
78 oen0 8582 . . . . . . . . . . . . . . . . . 18 (((ฯ‰ โˆˆ On โˆง ๐ท โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ท))
7977, 29, 78sylancl 585 . . . . . . . . . . . . . . . . 17 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o ๐ท))
8077, 9syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ท) โˆˆ On)
81 1onn 8636 . . . . . . . . . . . . . . . . . . 19 1o โˆˆ ฯ‰
82 ondif2 8498 . . . . . . . . . . . . . . . . . . 19 (ฯ‰ โˆˆ (On โˆ– 2o) โ†” (ฯ‰ โˆˆ On โˆง 1o โˆˆ ฯ‰))
838, 81, 82mpbir2an 708 . . . . . . . . . . . . . . . . . 18 ฯ‰ โˆˆ (On โˆ– 2o)
84 oeordi 8583 . . . . . . . . . . . . . . . . . 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 8518 . . . . . . . . . . . . . . . . . . 19 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o โˆ…) = 1o)
888, 87ax-mp 5 . . . . . . . . . . . . . . . . . 18 (ฯ‰ โ†‘o โˆ…) = 1o
8988eqcomi 2733 . . . . . . . . . . . . . . . . 17 1o = (ฯ‰ โ†‘o โˆ…)
9089a1i 11 . . . . . . . . . . . . . . . 16 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ 1o = (ฯ‰ โ†‘o โˆ…))
9186, 90, 73eltr4d 2840 . . . . . . . . . . . . . . 15 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ 1o โˆˆ ๐ถ)
92 oveq1 7409 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = 1o โ†’ (๐‘ฅ ยทo ๐ถ) = (1o ยทo ๐ถ))
93 om1r 8539 . . . . . . . . . . . . . . . . . 18 (๐ถ โˆˆ On โ†’ (1o ยทo ๐ถ) = ๐ถ)
9415, 93syl 17 . . . . . . . . . . . . . . . . 17 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (1o ยทo ๐ถ) = ๐ถ)
9592, 94sylan9eqr 2786 . . . . . . . . . . . . . . . 16 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ = 1o) โ†’ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
9695sseq2d 4007 . . . . . . . . . . . . . . 15 (((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โˆง ๐‘ฅ = 1o) โ†’ (๐ถ โІ (๐‘ฅ ยทo ๐ถ) โ†” ๐ถ โІ ๐ถ))
97 ssidd 3998 . . . . . . . . . . . . . . 15 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ โІ ๐ถ)
9891, 96, 97rspcedvd 3606 . . . . . . . . . . . . . 14 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ถ ๐ถ โІ (๐‘ฅ ยทo ๐ถ))
99 ssiun 5040 . . . . . . . . . . . . . 14 (โˆƒ๐‘ฅ โˆˆ ๐ถ ๐ถ โІ (๐‘ฅ ยทo ๐ถ) โ†’ ๐ถ โІ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
10098, 99syl 17 . . . . . . . . . . . . 13 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ ๐ถ โІ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ))
10175, 100eqssd 3992 . . . . . . . . . . . 12 ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
102101adantl 481 . . . . . . . . . . 11 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ โˆช ๐‘ฅ โˆˆ ๐ถ (๐‘ฅ ยทo ๐ถ) = ๐ถ)
10352, 102eleqtrd 2827 . . . . . . . . . 10 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
104103ex 412 . . . . . . . . 9 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
1051043expia 1118 . . . . . . . 8 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ (โˆ… โˆˆ ๐ด โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)))
106105com23 86 . . . . . . 7 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)))
107106imp 406 . . . . . 6 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (โˆ… โˆˆ ๐ด โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
10837, 107jaod 856 . . . . 5 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ ((๐ด = โˆ… โˆจ โˆ… โˆˆ ๐ด) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
10920, 108mpd 15 . . . 4 (((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โˆง (๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On)) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ)
110109ex 412 . . 3 ((๐ด โˆˆ ๐ถ โˆง ๐ต โˆˆ ๐ถ) โ†’ ((๐ถ = (ฯ‰ โ†‘o (ฯ‰ โ†‘o ๐ท)) โˆง ๐ท โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ ๐ถ))
1116, 110jaod 856 . 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 844   โˆจ w3o 1083   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  โˆƒwrex 3062   โˆ– cdif 3938   โІ wss 3941  โˆ…c0 4315  โˆช ciun 4988  Oncon0 6355  (class class class)co 7402  ฯ‰com 7849  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  ax-reg 9584  ax-inf2 9633
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-rmo 3368  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-ot 4630  df-uni 4901  df-int 4942  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-1st 7969  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:  omcl3g  42634
  Copyright terms: Public domain W3C validator