Step | Hyp | Ref
| Expression |
1 | | djueq2 9900 |
. . . . . . 7
β’ (π₯ = π΅ β (π΄ β π₯) = (π΄ β π΅)) |
2 | | oveq2 7416 |
. . . . . . 7
β’ (π₯ = π΅ β (π΄ +o π₯) = (π΄ +o π΅)) |
3 | 1, 2 | breq12d 5161 |
. . . . . 6
β’ (π₯ = π΅ β ((π΄ β π₯) β (π΄ +o π₯) β (π΄ β π΅) β (π΄ +o π΅))) |
4 | 3 | imbi2d 340 |
. . . . 5
β’ (π₯ = π΅ β ((π΄ β Ο β (π΄ β π₯) β (π΄ +o π₯)) β (π΄ β Ο β (π΄ β π΅) β (π΄ +o π΅)))) |
5 | | djueq2 9900 |
. . . . . . 7
β’ (π₯ = β
β (π΄ β π₯) = (π΄ β β
)) |
6 | | oveq2 7416 |
. . . . . . 7
β’ (π₯ = β
β (π΄ +o π₯) = (π΄ +o β
)) |
7 | 5, 6 | breq12d 5161 |
. . . . . 6
β’ (π₯ = β
β ((π΄ β π₯) β (π΄ +o π₯) β (π΄ β β
) β (π΄ +o
β
))) |
8 | | djueq2 9900 |
. . . . . . 7
β’ (π₯ = π¦ β (π΄ β π₯) = (π΄ β π¦)) |
9 | | oveq2 7416 |
. . . . . . 7
β’ (π₯ = π¦ β (π΄ +o π₯) = (π΄ +o π¦)) |
10 | 8, 9 | breq12d 5161 |
. . . . . 6
β’ (π₯ = π¦ β ((π΄ β π₯) β (π΄ +o π₯) β (π΄ β π¦) β (π΄ +o π¦))) |
11 | | djueq2 9900 |
. . . . . . 7
β’ (π₯ = suc π¦ β (π΄ β π₯) = (π΄ β suc π¦)) |
12 | | oveq2 7416 |
. . . . . . 7
β’ (π₯ = suc π¦ β (π΄ +o π₯) = (π΄ +o suc π¦)) |
13 | 11, 12 | breq12d 5161 |
. . . . . 6
β’ (π₯ = suc π¦ β ((π΄ β π₯) β (π΄ +o π₯) β (π΄ β suc π¦) β (π΄ +o suc π¦))) |
14 | | dju0en 10169 |
. . . . . . 7
β’ (π΄ β Ο β (π΄ β β
) β π΄) |
15 | | nna0 8603 |
. . . . . . 7
β’ (π΄ β Ο β (π΄ +o β
) = π΄) |
16 | 14, 15 | breqtrrd 5176 |
. . . . . 6
β’ (π΄ β Ο β (π΄ β β
) β
(π΄ +o
β
)) |
17 | | 1oex 8475 |
. . . . . . . . . . 11
β’
1o β V |
18 | | djuassen 10172 |
. . . . . . . . . . 11
β’ ((π΄ β Ο β§ π¦ β Ο β§
1o β V) β ((π΄ β π¦) β 1o) β (π΄ β (π¦ β 1o))) |
19 | 17, 18 | mp3an3 1450 |
. . . . . . . . . 10
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ β π¦) β 1o) β (π΄ β (π¦ β 1o))) |
20 | | enrefg 8979 |
. . . . . . . . . . 11
β’ (π΄ β Ο β π΄ β π΄) |
21 | | nnord 7862 |
. . . . . . . . . . . . 13
β’ (π¦ β Ο β Ord π¦) |
22 | | ordirr 6382 |
. . . . . . . . . . . . 13
β’ (Ord
π¦ β Β¬ π¦ β π¦) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β Ο β Β¬
π¦ β π¦) |
24 | | dju1en 10165 |
. . . . . . . . . . . 12
β’ ((π¦ β Ο β§ Β¬
π¦ β π¦) β (π¦ β 1o) β suc π¦) |
25 | 23, 24 | mpdan 685 |
. . . . . . . . . . 11
β’ (π¦ β Ο β (π¦ β 1o) β
suc π¦) |
26 | | djuen 10163 |
. . . . . . . . . . 11
β’ ((π΄ β π΄ β§ (π¦ β 1o) β suc π¦) β (π΄ β (π¦ β 1o)) β (π΄ β suc π¦)) |
27 | 20, 25, 26 | syl2an 596 |
. . . . . . . . . 10
β’ ((π΄ β Ο β§ π¦ β Ο) β (π΄ β (π¦ β 1o)) β (π΄ β suc π¦)) |
28 | | entr 9001 |
. . . . . . . . . 10
β’ ((((π΄ β π¦) β 1o) β (π΄ β (π¦ β 1o)) β§ (π΄ β (π¦ β 1o)) β (π΄ β suc π¦)) β ((π΄ β π¦) β 1o) β (π΄ β suc π¦)) |
29 | 19, 27, 28 | syl2anc 584 |
. . . . . . . . 9
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ β π¦) β 1o) β (π΄ β suc π¦)) |
30 | 29 | ensymd 9000 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π¦ β Ο) β (π΄ β suc π¦) β ((π΄ β π¦) β 1o)) |
31 | 17 | enref 8980 |
. . . . . . . . . . . 12
β’
1o β 1o |
32 | | djuen 10163 |
. . . . . . . . . . . 12
β’ (((π΄ β π¦) β (π΄ +o π¦) β§ 1o β 1o)
β ((π΄ β π¦) β 1o)
β ((π΄ +o
π¦) β
1o)) |
33 | 31, 32 | mpan2 689 |
. . . . . . . . . . 11
β’ ((π΄ β π¦) β (π΄ +o π¦) β ((π΄ β π¦) β 1o) β ((π΄ +o π¦) β
1o)) |
34 | 33 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ β π¦) β (π΄ +o π¦) β ((π΄ β π¦) β 1o) β ((π΄ +o π¦) β
1o))) |
35 | | nnacl 8610 |
. . . . . . . . . . . 12
β’ ((π΄ β Ο β§ π¦ β Ο) β (π΄ +o π¦) β
Ο) |
36 | | nnord 7862 |
. . . . . . . . . . . . 13
β’ ((π΄ +o π¦) β Ο β Ord
(π΄ +o π¦)) |
37 | | ordirr 6382 |
. . . . . . . . . . . . 13
β’ (Ord
(π΄ +o π¦) β Β¬ (π΄ +o π¦) β (π΄ +o π¦)) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π΄ β Ο β§ π¦ β Ο) β Β¬
(π΄ +o π¦) β (π΄ +o π¦)) |
39 | | dju1en 10165 |
. . . . . . . . . . . 12
β’ (((π΄ +o π¦) β Ο β§ Β¬
(π΄ +o π¦) β (π΄ +o π¦)) β ((π΄ +o π¦) β 1o) β suc (π΄ +o π¦)) |
40 | 35, 38, 39 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ +o π¦) β 1o)
β suc (π΄
+o π¦)) |
41 | | nnasuc 8605 |
. . . . . . . . . . 11
β’ ((π΄ β Ο β§ π¦ β Ο) β (π΄ +o suc π¦) = suc (π΄ +o π¦)) |
42 | 40, 41 | breqtrrd 5176 |
. . . . . . . . . 10
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ +o π¦) β 1o)
β (π΄ +o
suc π¦)) |
43 | 34, 42 | jctird 527 |
. . . . . . . . 9
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ β π¦) β (π΄ +o π¦) β (((π΄ β π¦) β 1o) β ((π΄ +o π¦) β 1o) β§
((π΄ +o π¦) β 1o)
β (π΄ +o
suc π¦)))) |
44 | | entr 9001 |
. . . . . . . . 9
β’ ((((π΄ β π¦) β 1o) β ((π΄ +o π¦) β 1o) β§
((π΄ +o π¦) β 1o)
β (π΄ +o
suc π¦)) β ((π΄ β π¦) β 1o) β (π΄ +o suc π¦)) |
45 | 43, 44 | syl6 35 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ β π¦) β (π΄ +o π¦) β ((π΄ β π¦) β 1o) β (π΄ +o suc π¦))) |
46 | | entr 9001 |
. . . . . . . 8
β’ (((π΄ β suc π¦) β ((π΄ β π¦) β 1o) β§ ((π΄ β π¦) β 1o) β (π΄ +o suc π¦)) β (π΄ β suc π¦) β (π΄ +o suc π¦)) |
47 | 30, 45, 46 | syl6an 682 |
. . . . . . 7
β’ ((π΄ β Ο β§ π¦ β Ο) β ((π΄ β π¦) β (π΄ +o π¦) β (π΄ β suc π¦) β (π΄ +o suc π¦))) |
48 | 47 | expcom 414 |
. . . . . 6
β’ (π¦ β Ο β (π΄ β Ο β ((π΄ β π¦) β (π΄ +o π¦) β (π΄ β suc π¦) β (π΄ +o suc π¦)))) |
49 | 7, 10, 13, 16, 48 | finds2 7890 |
. . . . 5
β’ (π₯ β Ο β (π΄ β Ο β (π΄ β π₯) β (π΄ +o π₯))) |
50 | 4, 49 | vtoclga 3565 |
. . . 4
β’ (π΅ β Ο β (π΄ β Ο β (π΄ β π΅) β (π΄ +o π΅))) |
51 | 50 | impcom 408 |
. . 3
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅) β (π΄ +o π΅)) |
52 | | carden2b 9961 |
. . 3
β’ ((π΄ β π΅) β (π΄ +o π΅) β (cardβ(π΄ β π΅)) = (cardβ(π΄ +o π΅))) |
53 | 51, 52 | syl 17 |
. 2
β’ ((π΄ β Ο β§ π΅ β Ο) β
(cardβ(π΄ β
π΅)) = (cardβ(π΄ +o π΅))) |
54 | | nnacl 8610 |
. . 3
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ +o π΅) β Ο) |
55 | | cardnn 9957 |
. . 3
β’ ((π΄ +o π΅) β Ο β (cardβ(π΄ +o π΅)) = (π΄ +o π΅)) |
56 | 54, 55 | syl 17 |
. 2
β’ ((π΄ β Ο β§ π΅ β Ο) β
(cardβ(π΄
+o π΅)) = (π΄ +o π΅)) |
57 | 53, 56 | eqtrd 2772 |
1
β’ ((π΄ β Ο β§ π΅ β Ο) β
(cardβ(π΄ β
π΅)) = (π΄ +o π΅)) |