Step | Hyp | Ref
| Expression |
1 | | eloni 6332 |
. . . . . . . . 9
โข (๐ต โ On โ Ord ๐ต) |
2 | 1 | ad2antlr 726 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ Ord ๐ต) |
3 | | simprl 770 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ๐ฅ โ ๐ต) |
4 | | ordsucss 7758 |
. . . . . . . 8
โข (Ord
๐ต โ (๐ฅ โ ๐ต โ suc ๐ฅ โ ๐ต)) |
5 | 2, 3, 4 | sylc 65 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ suc ๐ฅ โ ๐ต) |
6 | | onelon 6347 |
. . . . . . . . . 10
โข ((๐ต โ On โง ๐ฅ โ ๐ต) โ ๐ฅ โ On) |
7 | 6 | ad2ant2lr 747 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ๐ฅ โ On) |
8 | | onsuc 7751 |
. . . . . . . . 9
โข (๐ฅ โ On โ suc ๐ฅ โ On) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ suc ๐ฅ โ On) |
10 | | simplr 768 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ๐ต โ On) |
11 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ๐ด โ On) |
12 | | omwordi 8523 |
. . . . . . . 8
โข ((suc
๐ฅ โ On โง ๐ต โ On โง ๐ด โ On) โ (suc ๐ฅ โ ๐ต โ (๐ด ยทo suc ๐ฅ) โ (๐ด ยทo ๐ต))) |
13 | 9, 10, 11, 12 | syl3anc 1372 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ (suc ๐ฅ โ ๐ต โ (๐ด ยทo suc ๐ฅ) โ (๐ด ยทo ๐ต))) |
14 | 5, 13 | mpd 15 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ (๐ด ยทo suc ๐ฅ) โ (๐ด ยทo ๐ต)) |
15 | | simprr 772 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ๐ฆ โ ๐ด) |
16 | | onelon 6347 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ฆ โ ๐ด) โ ๐ฆ โ On) |
17 | 16 | ad2ant2rl 748 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ๐ฆ โ On) |
18 | | omcl 8487 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ฅ โ On) โ (๐ด ยทo ๐ฅ) โ On) |
19 | 11, 7, 18 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ (๐ด ยทo ๐ฅ) โ On) |
20 | | oaord 8499 |
. . . . . . . . 9
โข ((๐ฆ โ On โง ๐ด โ On โง (๐ด ยทo ๐ฅ) โ On) โ (๐ฆ โ ๐ด โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ ((๐ด ยทo ๐ฅ) +o ๐ด))) |
21 | 17, 11, 19, 20 | syl3anc 1372 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ (๐ฆ โ ๐ด โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ ((๐ด ยทo ๐ฅ) +o ๐ด))) |
22 | 15, 21 | mpbid 231 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ ((๐ด ยทo ๐ฅ) +o ๐ด)) |
23 | | omsuc 8477 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ฅ โ On) โ (๐ด ยทo suc ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ด)) |
24 | 11, 7, 23 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ (๐ด ยทo suc ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ด)) |
25 | 22, 24 | eleqtrrd 2841 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo suc ๐ฅ)) |
26 | 14, 25 | sseldd 3950 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ด)) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) |
27 | 26 | ralrimivva 3198 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) |
28 | | omxpenlem.1 |
. . . . 5
โข ๐น = (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ด ยทo ๐ฅ) +o ๐ฆ)) |
29 | 28 | fmpo 8005 |
. . . 4
โข
(โ๐ฅ โ
๐ต โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โ ๐น:(๐ต ร ๐ด)โถ(๐ด ยทo ๐ต)) |
30 | 27, 29 | sylib 217 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ ๐น:(๐ต ร ๐ด)โถ(๐ด ยทo ๐ต)) |
31 | 30 | ffnd 6674 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ ๐น Fn (๐ต ร ๐ด)) |
32 | | simpll 766 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ ๐ด โ On) |
33 | | omcl 8487 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |
34 | | onelon 6347 |
. . . . . . . 8
โข (((๐ด ยทo ๐ต) โ On โง ๐ โ (๐ด ยทo ๐ต)) โ ๐ โ On) |
35 | 33, 34 | sylan 581 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ ๐ โ On) |
36 | | noel 4295 |
. . . . . . . . . . . 12
โข ยฌ
๐ โ
โ
|
37 | | oveq1 7369 |
. . . . . . . . . . . . . 14
โข (๐ด = โ
โ (๐ด ยทo ๐ต) = (โ
ยทo ๐ต)) |
38 | | om0r 8490 |
. . . . . . . . . . . . . 14
โข (๐ต โ On โ (โ
ยทo ๐ต) =
โ
) |
39 | 37, 38 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ด = โ
) โ (๐ด ยทo ๐ต) = โ
) |
40 | 39 | eleq2d 2824 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง ๐ด = โ
) โ (๐ โ (๐ด ยทo ๐ต) โ ๐ โ โ
)) |
41 | 36, 40 | mtbiri 327 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ด = โ
) โ ยฌ ๐ โ (๐ด ยทo ๐ต)) |
42 | 41 | ex 414 |
. . . . . . . . . 10
โข (๐ต โ On โ (๐ด = โ
โ ยฌ ๐ โ (๐ด ยทo ๐ต))) |
43 | 42 | necon2ad 2959 |
. . . . . . . . 9
โข (๐ต โ On โ (๐ โ (๐ด ยทo ๐ต) โ ๐ด โ โ
)) |
44 | 43 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (๐ โ (๐ด ยทo ๐ต) โ ๐ด โ โ
)) |
45 | 44 | imp 408 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ ๐ด โ โ
) |
46 | | omeu 8537 |
. . . . . . 7
โข ((๐ด โ On โง ๐ โ On โง ๐ด โ โ
) โ
โ!๐โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐)) |
47 | 32, 35, 45, 46 | syl3anc 1372 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ โ!๐โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐)) |
48 | | vex 3452 |
. . . . . . . . 9
โข ๐ โ V |
49 | | vex 3452 |
. . . . . . . . 9
โข ๐ โ V |
50 | 48, 49 | brcnv 5843 |
. . . . . . . 8
โข (๐โก๐น๐ โ ๐๐น๐) |
51 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ โ (๐ด ยทo ๐ต) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต))) |
52 | 51 | biimpac 480 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (๐ด ยทo ๐ต) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) |
53 | 6 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ต โ On โ (๐ฅ โ ๐ต โ ๐ฅ โ On)) |
54 | 53 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โ (๐ฅ โ ๐ต โ ๐ฅ โ On)) |
55 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ ๐ด โ On) |
56 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ ๐ฅ โ On) |
57 | 55, 56, 18 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (๐ด ยทo ๐ฅ) โ On) |
58 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ ๐ฆ โ ๐ด) |
59 | 55, 58, 16 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ ๐ฆ โ On) |
60 | | oaword1 8504 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ด ยทo ๐ฅ) โ On โง ๐ฆ โ On) โ (๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ)) |
61 | 57, 59, 60 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ)) |
62 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) |
63 | 33 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (๐ด ยทo ๐ต) โ On) |
64 | | ontr2 6369 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ด ยทo ๐ฅ) โ On โง (๐ด ยทo ๐ต) โ On) โ (((๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) โ (๐ด ยทo ๐ฅ) โ (๐ด ยทo ๐ต))) |
65 | 57, 63, 64 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (((๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) โ (๐ด ยทo ๐ฅ) โ (๐ด ยทo ๐ต))) |
66 | 61, 62, 65 | mp2and 698 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (๐ด ยทo ๐ฅ) โ (๐ด ยทo ๐ต)) |
67 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ ๐ต โ On) |
68 | 62 | ne0d 4300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (๐ด ยทo ๐ต) โ โ
) |
69 | | on0eln0 6378 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ด ยทo ๐ต) โ On โ (โ
โ (๐ด
ยทo ๐ต)
โ (๐ด
ยทo ๐ต)
โ โ
)) |
70 | 63, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (โ
โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ต) โ โ
)) |
71 | 68, 70 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ โ
โ (๐ด ยทo ๐ต)) |
72 | | om00el 8528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด โ On โง ๐ต โ On) โ (โ
โ (๐ด
ยทo ๐ต)
โ (โ
โ ๐ด
โง โ
โ ๐ต))) |
73 | 72 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (โ
โ (๐ด ยทo ๐ต) โ (โ
โ ๐ด โง โ
โ ๐ต))) |
74 | 71, 73 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (โ
โ ๐ด โง โ
โ ๐ต)) |
75 | 74 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ โ
โ ๐ด) |
76 | | omord2 8519 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ On โง ๐ต โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (๐ฅ โ ๐ต โ (๐ด ยทo ๐ฅ) โ (๐ด ยทo ๐ต))) |
77 | 56, 67, 55, 75, 76 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ (๐ฅ โ ๐ต โ (๐ด ยทo ๐ฅ) โ (๐ด ยทo ๐ต))) |
78 | 66, 77 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โง ๐ฅ โ On) โ ๐ฅ โ ๐ต) |
79 | 78 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โ (๐ฅ โ On โ ๐ฅ โ ๐ต)) |
80 | 54, 79 | impbid 211 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ On โง ๐ต โ On) โง (((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต) โง ๐ฆ โ ๐ด)) โ (๐ฅ โ ๐ต โ ๐ฅ โ On)) |
81 | 80 | expr 458 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ On โง ๐ต โ On) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) โ (๐ฆ โ ๐ด โ (๐ฅ โ ๐ต โ ๐ฅ โ On))) |
82 | 81 | pm5.32rd 579 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ On โง ๐ต โ On) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ (๐ด ยทo ๐ต)) โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โ (๐ฅ โ On โง ๐ฆ โ ๐ด))) |
83 | 52, 82 | sylan2 594 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On) โง (๐ โ (๐ด ยทo ๐ต) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ))) โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โ (๐ฅ โ On โง ๐ฆ โ ๐ด))) |
84 | 83 | expr 458 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ (๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โ (๐ฅ โ On โง ๐ฆ โ ๐ด)))) |
85 | 84 | pm5.32rd 579 |
. . . . . . . . . . . . 13
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ (((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)) โ ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))) |
86 | | eqcom 2744 |
. . . . . . . . . . . . . 14
โข (๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐) |
87 | 86 | anbi2i 624 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ On โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)) โ ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐)) |
88 | 85, 87 | bitrdi 287 |
. . . . . . . . . . . 12
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ (((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)) โ ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐))) |
89 | 88 | anbi2d 630 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ ((๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ))) โ (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐)))) |
90 | | an12 644 |
. . . . . . . . . . 11
โข ((๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐)) โ ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐))) |
91 | 89, 90 | bitrdi 287 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ ((๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ))) โ ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐)))) |
92 | 91 | 2exbidv 1928 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ (โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ))) โ โ๐ฅโ๐ฆ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐)))) |
93 | | df-mpo 7367 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ด ยทo ๐ฅ) +o ๐ฆ)) = {โจโจ๐ฅ, ๐ฆโฉ, ๐โฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ))} |
94 | | dfoprab2 7420 |
. . . . . . . . . . . 12
โข
{โจโจ๐ฅ,
๐ฆโฉ, ๐โฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ))} = {โจ๐, ๐โฉ โฃ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))} |
95 | 28, 93, 94 | 3eqtri 2769 |
. . . . . . . . . . 11
โข ๐น = {โจ๐, ๐โฉ โฃ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))} |
96 | 95 | breqi 5116 |
. . . . . . . . . 10
โข (๐๐น๐ โ ๐{โจ๐, ๐โฉ โฃ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))}๐) |
97 | | df-br 5111 |
. . . . . . . . . 10
โข (๐{โจ๐, ๐โฉ โฃ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))}๐ โ โจ๐, ๐โฉ โ {โจ๐, ๐โฉ โฃ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))}) |
98 | | opabidw 5486 |
. . . . . . . . . 10
โข
(โจ๐, ๐โฉ โ {โจ๐, ๐โฉ โฃ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))} โ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))) |
99 | 96, 97, 98 | 3bitri 297 |
. . . . . . . . 9
โข (๐๐น๐ โ โ๐ฅโ๐ฆ(๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ด) โง ๐ = ((๐ด ยทo ๐ฅ) +o ๐ฆ)))) |
100 | | r2ex 3193 |
. . . . . . . . 9
โข
(โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐) โ โ๐ฅโ๐ฆ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐))) |
101 | 92, 99, 100 | 3bitr4g 314 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ (๐๐น๐ โ โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐))) |
102 | 50, 101 | bitrid 283 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ (๐โก๐น๐ โ โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐))) |
103 | 102 | eubidv 2585 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ (โ!๐ ๐โก๐น๐ โ โ!๐โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐))) |
104 | 47, 103 | mpbird 257 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง ๐ โ (๐ด ยทo ๐ต)) โ โ!๐ ๐โก๐น๐) |
105 | 104 | ralrimiva 3144 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ โ๐ โ (๐ด ยทo ๐ต)โ!๐ ๐โก๐น๐) |
106 | | fnres 6633 |
. . . 4
โข ((โก๐น โพ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ โ๐ โ (๐ด ยทo ๐ต)โ!๐ ๐โก๐น๐) |
107 | 105, 106 | sylibr 233 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ (โก๐น โพ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต)) |
108 | | relcnv 6061 |
. . . . 5
โข Rel โก๐น |
109 | | df-rn 5649 |
. . . . . 6
โข ran ๐น = dom โก๐น |
110 | 30 | frnd 6681 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ ran ๐น โ (๐ด ยทo ๐ต)) |
111 | 109, 110 | eqsstrrid 3998 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ dom โก๐น โ (๐ด ยทo ๐ต)) |
112 | | relssres 5983 |
. . . . 5
โข ((Rel
โก๐น โง dom โก๐น โ (๐ด ยทo ๐ต)) โ (โก๐น โพ (๐ด ยทo ๐ต)) = โก๐น) |
113 | 108, 111,
112 | sylancr 588 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ (โก๐น โพ (๐ด ยทo ๐ต)) = โก๐น) |
114 | 113 | fneq1d 6600 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ ((โก๐น โพ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ โก๐น Fn (๐ด ยทo ๐ต))) |
115 | 107, 114 | mpbid 231 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ โก๐น Fn (๐ด ยทo ๐ต)) |
116 | | dff1o4 6797 |
. 2
โข (๐น:(๐ต ร ๐ด)โ1-1-ontoโ(๐ด ยทo ๐ต) โ (๐น Fn (๐ต ร ๐ด) โง โก๐น Fn (๐ด ยทo ๐ต))) |
117 | 31, 115, 116 | sylanbrc 584 |
1
โข ((๐ด โ On โง ๐ต โ On) โ ๐น:(๐ต ร ๐ด)โ1-1-ontoโ(๐ด ยทo ๐ต)) |