Step | Hyp | Ref
| Expression |
1 | | oa00 8559 |
. . . . . . . . 9
โข ((๐ต โ On โง ๐ถ โ On) โ ((๐ต +o ๐ถ) = โ
โ (๐ต = โ
โง ๐ถ = โ
))) |
2 | 1 | biimpar 479 |
. . . . . . . 8
โข (((๐ต โ On โง ๐ถ โ On) โง (๐ต = โ
โง ๐ถ = โ
)) โ (๐ต +o ๐ถ) = โ
) |
3 | 2 | oveq2d 7425 |
. . . . . . 7
โข (((๐ต โ On โง ๐ถ โ On) โง (๐ต = โ
โง ๐ถ = โ
)) โ (โ
โo (๐ต
+o ๐ถ)) =
(โ
โo โ
)) |
4 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ต = โ
โ (โ
โo ๐ต) =
(โ
โo โ
)) |
5 | | oveq2 7417 |
. . . . . . . . . . 11
โข (๐ถ = โ
โ (โ
โo ๐ถ) =
(โ
โo โ
)) |
6 | | oe0m0 8520 |
. . . . . . . . . . 11
โข (โ
โo โ
) = 1o |
7 | 5, 6 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ถ = โ
โ (โ
โo ๐ถ) =
1o) |
8 | 4, 7 | oveqan12d 7428 |
. . . . . . . . 9
โข ((๐ต = โ
โง ๐ถ = โ
) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = ((โ
โo โ
)
ยทo 1o)) |
9 | | 0elon 6419 |
. . . . . . . . . . 11
โข โ
โ On |
10 | | oecl 8537 |
. . . . . . . . . . 11
โข ((โ
โ On โง โ
โ On) โ (โ
โo โ
)
โ On) |
11 | 9, 9, 10 | mp2an 691 |
. . . . . . . . . 10
โข (โ
โo โ
) โ On |
12 | | om1 8542 |
. . . . . . . . . 10
โข ((โ
โo โ
) โ On โ ((โ
โo
โ
) ยทo 1o) = (โ
โo
โ
)) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
โข ((โ
โo โ
) ยทo 1o) = (โ
โo โ
) |
14 | 8, 13 | eqtrdi 2789 |
. . . . . . . 8
โข ((๐ต = โ
โง ๐ถ = โ
) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = (โ
โo
โ
)) |
15 | 14 | adantl 483 |
. . . . . . 7
โข (((๐ต โ On โง ๐ถ โ On) โง (๐ต = โ
โง ๐ถ = โ
)) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = (โ
โo
โ
)) |
16 | 3, 15 | eqtr4d 2776 |
. . . . . 6
โข (((๐ต โ On โง ๐ถ โ On) โง (๐ต = โ
โง ๐ถ = โ
)) โ (โ
โo (๐ต
+o ๐ถ)) =
((โ
โo ๐ต) ยทo (โ
โo ๐ถ))) |
17 | | oacl 8535 |
. . . . . . . . . 10
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ต +o ๐ถ) โ On) |
18 | | on0eln0 6421 |
. . . . . . . . . 10
โข ((๐ต +o ๐ถ) โ On โ (โ
โ (๐ต +o ๐ถ) โ (๐ต +o ๐ถ) โ โ
)) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โ (๐ต +o
๐ถ) โ (๐ต +o ๐ถ) โ โ
)) |
20 | | oe0m1 8521 |
. . . . . . . . . 10
โข ((๐ต +o ๐ถ) โ On โ (โ
โ (๐ต +o ๐ถ) โ (โ
โo (๐ต +o ๐ถ)) = โ
)) |
21 | 17, 20 | syl 17 |
. . . . . . . . 9
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โ (๐ต +o
๐ถ) โ (โ
โo (๐ต
+o ๐ถ)) =
โ
)) |
22 | 1 | necon3abid 2978 |
. . . . . . . . 9
โข ((๐ต โ On โง ๐ถ โ On) โ ((๐ต +o ๐ถ) โ โ
โ ยฌ (๐ต = โ
โง ๐ถ = โ
))) |
23 | 19, 21, 22 | 3bitr3d 309 |
. . . . . . . 8
โข ((๐ต โ On โง ๐ถ โ On) โ ((โ
โo (๐ต
+o ๐ถ)) = โ
โ ยฌ (๐ต = โ
โง ๐ถ =
โ
))) |
24 | 23 | biimpar 479 |
. . . . . . 7
โข (((๐ต โ On โง ๐ถ โ On) โง ยฌ (๐ต = โ
โง ๐ถ = โ
)) โ (โ
โo (๐ต
+o ๐ถ)) =
โ
) |
25 | | on0eln0 6421 |
. . . . . . . . . . . 12
โข (๐ต โ On โ (โ
โ ๐ต โ ๐ต โ โ
)) |
26 | 25 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ต โ ๐ต โ โ
)) |
27 | | on0eln0 6421 |
. . . . . . . . . . . 12
โข (๐ถ โ On โ (โ
โ ๐ถ โ ๐ถ โ โ
)) |
28 | 27 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ถ โ ๐ถ โ โ
)) |
29 | 26, 28 | orbi12d 918 |
. . . . . . . . . 10
โข ((๐ต โ On โง ๐ถ โ On) โ ((โ
โ ๐ต โจ โ
โ ๐ถ) โ (๐ต โ โ
โจ ๐ถ โ
โ
))) |
30 | | neorian 3038 |
. . . . . . . . . 10
โข ((๐ต โ โ
โจ ๐ถ โ โ
) โ ยฌ
(๐ต = โ
โง ๐ถ = โ
)) |
31 | 29, 30 | bitrdi 287 |
. . . . . . . . 9
โข ((๐ต โ On โง ๐ถ โ On) โ ((โ
โ ๐ต โจ โ
โ ๐ถ) โ ยฌ
(๐ต = โ
โง ๐ถ = โ
))) |
32 | | oe0m1 8521 |
. . . . . . . . . . . . . . 15
โข (๐ต โ On โ (โ
โ ๐ต โ (โ
โo ๐ต) =
โ
)) |
33 | 32 | biimpa 478 |
. . . . . . . . . . . . . 14
โข ((๐ต โ On โง โ
โ
๐ต) โ (โ
โo ๐ต) =
โ
) |
34 | 33 | oveq1d 7424 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง โ
โ
๐ต) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = (โ
ยทo (โ
โo ๐ถ))) |
35 | | oecl 8537 |
. . . . . . . . . . . . . . 15
โข ((โ
โ On โง ๐ถ โ
On) โ (โ
โo ๐ถ) โ On) |
36 | 9, 35 | mpan 689 |
. . . . . . . . . . . . . 14
โข (๐ถ โ On โ (โ
โo ๐ถ)
โ On) |
37 | | om0r 8539 |
. . . . . . . . . . . . . 14
โข ((โ
โo ๐ถ)
โ On โ (โ
ยทo (โ
โo
๐ถ)) =
โ
) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ถ โ On โ (โ
ยทo (โ
โo ๐ถ)) = โ
) |
39 | 34, 38 | sylan9eq 2793 |
. . . . . . . . . . . 12
โข (((๐ต โ On โง โ
โ
๐ต) โง ๐ถ โ On) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
) |
40 | 39 | an32s 651 |
. . . . . . . . . . 11
โข (((๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ต) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
) |
41 | | oe0m1 8521 |
. . . . . . . . . . . . . . 15
โข (๐ถ โ On โ (โ
โ ๐ถ โ (โ
โo ๐ถ) =
โ
)) |
42 | 41 | biimpa 478 |
. . . . . . . . . . . . . 14
โข ((๐ถ โ On โง โ
โ
๐ถ) โ (โ
โo ๐ถ) =
โ
) |
43 | 42 | oveq2d 7425 |
. . . . . . . . . . . . 13
โข ((๐ถ โ On โง โ
โ
๐ถ) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = ((โ
โo ๐ต) ยทo
โ
)) |
44 | | oecl 8537 |
. . . . . . . . . . . . . . 15
โข ((โ
โ On โง ๐ต โ
On) โ (โ
โo ๐ต) โ On) |
45 | 9, 44 | mpan 689 |
. . . . . . . . . . . . . 14
โข (๐ต โ On โ (โ
โo ๐ต)
โ On) |
46 | | om0 8517 |
. . . . . . . . . . . . . 14
โข ((โ
โo ๐ต)
โ On โ ((โ
โo ๐ต) ยทo โ
) =
โ
) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ต โ On โ ((โ
โo ๐ต)
ยทo โ
) = โ
) |
48 | 43, 47 | sylan9eqr 2795 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง (๐ถ โ On โง โ
โ
๐ถ)) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
) |
49 | 48 | anassrs 469 |
. . . . . . . . . . 11
โข (((๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
) |
50 | 40, 49 | jaodan 957 |
. . . . . . . . . 10
โข (((๐ต โ On โง ๐ถ โ On) โง (โ
โ ๐ต โจ โ
โ ๐ถ)) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
) |
51 | 50 | ex 414 |
. . . . . . . . 9
โข ((๐ต โ On โง ๐ถ โ On) โ ((โ
โ ๐ต โจ โ
โ ๐ถ) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
)) |
52 | 31, 51 | sylbird 260 |
. . . . . . . 8
โข ((๐ต โ On โง ๐ถ โ On) โ (ยฌ (๐ต = โ
โง ๐ถ = โ
) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
)) |
53 | 52 | imp 408 |
. . . . . . 7
โข (((๐ต โ On โง ๐ถ โ On) โง ยฌ (๐ต = โ
โง ๐ถ = โ
)) โ ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ)) = โ
) |
54 | 24, 53 | eqtr4d 2776 |
. . . . . 6
โข (((๐ต โ On โง ๐ถ โ On) โง ยฌ (๐ต = โ
โง ๐ถ = โ
)) โ (โ
โo (๐ต
+o ๐ถ)) =
((โ
โo ๐ต) ยทo (โ
โo ๐ถ))) |
55 | 16, 54 | pm2.61dan 812 |
. . . . 5
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โo (๐ต
+o ๐ถ)) =
((โ
โo ๐ต) ยทo (โ
โo ๐ถ))) |
56 | | oveq1 7416 |
. . . . . 6
โข (๐ด = โ
โ (๐ด โo (๐ต +o ๐ถ)) = (โ
โo (๐ต +o ๐ถ))) |
57 | | oveq1 7416 |
. . . . . . 7
โข (๐ด = โ
โ (๐ด โo ๐ต) = (โ
โo
๐ต)) |
58 | | oveq1 7416 |
. . . . . . 7
โข (๐ด = โ
โ (๐ด โo ๐ถ) = (โ
โo
๐ถ)) |
59 | 57, 58 | oveq12d 7427 |
. . . . . 6
โข (๐ด = โ
โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ)) = ((โ
โo ๐ต)
ยทo (โ
โo ๐ถ))) |
60 | 56, 59 | eqeq12d 2749 |
. . . . 5
โข (๐ด = โ
โ ((๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ)) โ (โ
โo (๐ต +o ๐ถ)) = ((โ
โo ๐ต) ยทo (โ
โo ๐ถ)))) |
61 | 55, 60 | imbitrrid 245 |
. . . 4
โข (๐ด = โ
โ ((๐ต โ On โง ๐ถ โ On) โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ)))) |
62 | 61 | impcom 409 |
. . 3
โข (((๐ต โ On โง ๐ถ โ On) โง ๐ด = โ
) โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) |
63 | | oveq1 7416 |
. . . . . . . 8
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ (๐ด โo (๐ต +o ๐ถ)) = (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo (๐ต +o ๐ถ))) |
64 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ (๐ด โo ๐ต) = (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ต)) |
65 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ (๐ด โo ๐ถ) = (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ถ)) |
66 | 64, 65 | oveq12d 7427 |
. . . . . . . 8
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ)) = ((if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ต) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ))) |
67 | 63, 66 | eqeq12d 2749 |
. . . . . . 7
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ ((๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ)) โ (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo (๐ต +o ๐ถ)) = ((if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ต) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ)))) |
68 | 67 | imbi2d 341 |
. . . . . 6
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ ((๐ถ โ On โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) โ (๐ถ โ On โ (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo (๐ต +o ๐ถ)) = ((if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ต) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ))))) |
69 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ต = if(๐ต โ On, ๐ต, 1o) โ (๐ต +o ๐ถ) = (if(๐ต โ On, ๐ต, 1o) +o ๐ถ)) |
70 | 69 | oveq2d 7425 |
. . . . . . . 8
โข (๐ต = if(๐ต โ On, ๐ต, 1o) โ (if((๐ด โ On โง โ
โ
๐ด), ๐ด, 1o) โo (๐ต +o ๐ถ)) = (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo
(if(๐ต โ On, ๐ต, 1o) +o
๐ถ))) |
71 | | oveq2 7417 |
. . . . . . . . 9
โข (๐ต = if(๐ต โ On, ๐ต, 1o) โ (if((๐ด โ On โง โ
โ
๐ด), ๐ด, 1o) โo ๐ต) = (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo if(๐ต โ On, ๐ต, 1o))) |
72 | 71 | oveq1d 7424 |
. . . . . . . 8
โข (๐ต = if(๐ต โ On, ๐ต, 1o) โ ((if((๐ด โ On โง โ
โ
๐ด), ๐ด, 1o) โo ๐ต) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ)) =
((if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo if(๐ต
โ On, ๐ต,
1o)) ยทo (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ถ))) |
73 | 70, 72 | eqeq12d 2749 |
. . . . . . 7
โข (๐ต = if(๐ต โ On, ๐ต, 1o) โ ((if((๐ด โ On โง โ
โ
๐ด), ๐ด, 1o) โo (๐ต +o ๐ถ)) = ((if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ต) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ))
โ (if((๐ด โ On
โง โ
โ ๐ด),
๐ด, 1o)
โo (if(๐ต
โ On, ๐ต,
1o) +o ๐ถ)) = ((if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo if(๐ต โ On, ๐ต, 1o)) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ)))) |
74 | 73 | imbi2d 341 |
. . . . . 6
โข (๐ต = if(๐ต โ On, ๐ต, 1o) โ ((๐ถ โ On โ (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo (๐ต +o ๐ถ)) = ((if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo ๐ต) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ)))
โ (๐ถ โ On โ
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo (if(๐ต
โ On, ๐ต,
1o) +o ๐ถ)) = ((if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โo if(๐ต โ On, ๐ต, 1o)) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ))))) |
75 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ (๐ด โ On โ if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ
On)) |
76 | | eleq2 2823 |
. . . . . . . . . 10
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ (โ
โ
๐ด โ โ
โ
if((๐ด โ On โง
โ
โ ๐ด), ๐ด,
1o))) |
77 | 75, 76 | anbi12d 632 |
. . . . . . . . 9
โข (๐ด = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ ((๐ด โ On โง โ
โ ๐ด) โ (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ On โง โ
โ if((๐ด โ On
โง โ
โ ๐ด),
๐ด,
1o)))) |
78 | | eleq1 2822 |
. . . . . . . . . 10
โข
(1o = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ (1o
โ On โ if((๐ด
โ On โง โ
โ ๐ด), ๐ด, 1o) โ
On)) |
79 | | eleq2 2823 |
. . . . . . . . . 10
โข
(1o = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ (โ
โ
1o โ โ
โ if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o))) |
80 | 78, 79 | anbi12d 632 |
. . . . . . . . 9
โข
(1o = if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ ((1o
โ On โง โ
โ 1o) โ (if((๐ด โ On โง โ
โ ๐ด), ๐ด, 1o) โ On โง โ
โ if((๐ด โ On
โง โ
โ ๐ด),
๐ด,
1o)))) |
81 | | 1on 8478 |
. . . . . . . . . 10
โข
1o โ On |
82 | | 0lt1o 8504 |
. . . . . . . . . 10
โข โ
โ 1o |
83 | 81, 82 | pm3.2i 472 |
. . . . . . . . 9
โข
(1o โ On โง โ
โ
1o) |
84 | 77, 80, 83 | elimhyp 4594 |
. . . . . . . 8
โข
(if((๐ด โ On
โง โ
โ ๐ด),
๐ด, 1o) โ On
โง โ
โ if((๐ด
โ On โง โ
โ ๐ด), ๐ด, 1o)) |
85 | 84 | simpli 485 |
. . . . . . 7
โข if((๐ด โ On โง โ
โ
๐ด), ๐ด, 1o) โ On |
86 | 84 | simpri 487 |
. . . . . . 7
โข โ
โ if((๐ด โ On
โง โ
โ ๐ด),
๐ด,
1o) |
87 | 81 | elimel 4598 |
. . . . . . 7
โข if(๐ต โ On, ๐ต, 1o) โ On |
88 | 85, 86, 87 | oeoalem 8596 |
. . . . . 6
โข (๐ถ โ On โ (if((๐ด โ On โง โ
โ
๐ด), ๐ด, 1o) โo
(if(๐ต โ On, ๐ต, 1o) +o
๐ถ)) = ((if((๐ด โ On โง โ
โ
๐ด), ๐ด, 1o) โo if(๐ต โ On, ๐ต, 1o)) ยทo
(if((๐ด โ On โง
โ
โ ๐ด), ๐ด, 1o)
โo ๐ถ))) |
89 | 68, 74, 88 | dedth2h 4588 |
. . . . 5
โข (((๐ด โ On โง โ
โ
๐ด) โง ๐ต โ On) โ (๐ถ โ On โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ)))) |
90 | 89 | impr 456 |
. . . 4
โข (((๐ด โ On โง โ
โ
๐ด) โง (๐ต โ On โง ๐ถ โ On)) โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) |
91 | 90 | an32s 651 |
. . 3
โข (((๐ด โ On โง (๐ต โ On โง ๐ถ โ On)) โง โ
โ ๐ด) โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) |
92 | 62, 91 | oe0lem 8513 |
. 2
โข ((๐ด โ On โง (๐ต โ On โง ๐ถ โ On)) โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) |
93 | 92 | 3impb 1116 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) |