Step | Hyp | Ref
| Expression |
1 | | harcl 9554 |
. . . 4
β’
(harβπ΄) β
On |
2 | | simp3 1139 |
. . . 4
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π΄ β
GCH) |
3 | | djudoml 10179 |
. . . 4
β’
(((harβπ΄)
β On β§ π« π΄
β GCH) β (harβπ΄) βΌ ((harβπ΄) β π« π΄)) |
4 | 1, 2, 3 | sylancr 588 |
. . 3
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(harβπ΄) βΌ
((harβπ΄) β
π« π΄)) |
5 | | domnsym 9099 |
. . . . . . . . 9
β’ (Ο
βΌ π΄ β Β¬
π΄ βΊ
Ο) |
6 | 5 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β Β¬
π΄ βΊ
Ο) |
7 | | isfinite 9647 |
. . . . . . . 8
β’ (π΄ β Fin β π΄ βΊ
Ο) |
8 | 6, 7 | sylnibr 329 |
. . . . . . 7
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β Β¬
π΄ β
Fin) |
9 | | pwfi 9178 |
. . . . . . 7
β’ (π΄ β Fin β π«
π΄ β
Fin) |
10 | 8, 9 | sylnib 328 |
. . . . . 6
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β Β¬
π« π΄ β
Fin) |
11 | | djudoml 10179 |
. . . . . . 7
β’
((π« π΄ β
GCH β§ (harβπ΄)
β On) β π« π΄ βΌ (π« π΄ β (harβπ΄))) |
12 | 2, 1, 11 | sylancl 587 |
. . . . . 6
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π΄ βΌ
(π« π΄ β
(harβπ΄))) |
13 | | fvexd 6907 |
. . . . . . . . 9
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(harβπ΄) β
V) |
14 | | djuex 9903 |
. . . . . . . . 9
β’
((π« π΄ β
GCH β§ (harβπ΄)
β V) β (π« π΄ β (harβπ΄)) β V) |
15 | 2, 13, 14 | syl2anc 585 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
(harβπ΄)) β
V) |
16 | | canth2g 9131 |
. . . . . . . 8
β’
((π« π΄
β (harβπ΄))
β V β (π« π΄ β (harβπ΄)) βΊ π« (π« π΄ β (harβπ΄))) |
17 | 15, 16 | syl 17 |
. . . . . . 7
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
(harβπ΄)) βΊ
π« (π« π΄
β (harβπ΄))) |
18 | | pwdjuen 10176 |
. . . . . . . . 9
β’
((π« π΄ β
GCH β§ (harβπ΄)
β On) β π« (π« π΄ β (harβπ΄)) β (π« π« π΄ Γ π«
(harβπ΄))) |
19 | 2, 1, 18 | sylancl 587 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π« π΄
β (harβπ΄))
β (π« π« π΄ Γ π« (harβπ΄))) |
20 | 2 | pwexd 5378 |
. . . . . . . . . 10
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π« π΄
β V) |
21 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β π΄ β GCH) |
22 | | harwdom 9586 |
. . . . . . . . . . 11
β’ (π΄ β GCH β
(harβπ΄)
βΌ* π« (π΄ Γ π΄)) |
23 | | wdompwdom 9573 |
. . . . . . . . . . 11
β’
((harβπ΄)
βΌ* π« (π΄ Γ π΄) β π« (harβπ΄) βΌ π« π«
(π΄ Γ π΄)) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . . . 10
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (harβπ΄)
βΌ π« π« (π΄ Γ π΄)) |
25 | | xpdom2g 9068 |
. . . . . . . . . 10
β’
((π« π« π΄ β V β§ π« (harβπ΄) βΌ π« π«
(π΄ Γ π΄)) β (π« π«
π΄ Γ π«
(harβπ΄)) βΌ
(π« π« π΄
Γ π« π« (π΄ Γ π΄))) |
26 | 20, 24, 25 | syl2anc 585 |
. . . . . . . . 9
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π« π΄
Γ π« (harβπ΄)) βΌ (π« π« π΄ Γ π« π«
(π΄ Γ π΄))) |
27 | 21, 21 | xpexd 7738 |
. . . . . . . . . . . . 13
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ Γ π΄) β V) |
28 | 27 | pwexd 5378 |
. . . . . . . . . . . 12
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π΄ Γ π΄) β V) |
29 | | pwdjuen 10176 |
. . . . . . . . . . . 12
β’
((π« π΄ β
GCH β§ π« (π΄
Γ π΄) β V) β
π« (π« π΄
β π« (π΄
Γ π΄)) β
(π« π« π΄
Γ π« π« (π΄ Γ π΄))) |
30 | 2, 28, 29 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π« π΄
β π« (π΄
Γ π΄)) β
(π« π« π΄
Γ π« π« (π΄ Γ π΄))) |
31 | 30 | ensymd 9001 |
. . . . . . . . . 10
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π« π΄
Γ π« π« (π΄ Γ π΄)) β π« (π« π΄ β π« (π΄ Γ π΄))) |
32 | | enrefg 8980 |
. . . . . . . . . . . . . 14
β’
(π« π΄ β
GCH β π« π΄
β π« π΄) |
33 | 2, 32 | syl 17 |
. . . . . . . . . . . . 13
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π΄ β
π« π΄) |
34 | | gchxpidm 10664 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β (π΄ Γ π΄) β π΄) |
35 | 21, 8, 34 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ Γ π΄) β π΄) |
36 | | pwen 9150 |
. . . . . . . . . . . . . 14
β’ ((π΄ Γ π΄) β π΄ β π« (π΄ Γ π΄) β π« π΄) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π΄ Γ π΄) β π« π΄) |
38 | | djuen 10164 |
. . . . . . . . . . . . 13
β’
((π« π΄
β π« π΄ β§
π« (π΄ Γ π΄) β π« π΄) β (π« π΄ β π« (π΄ Γ π΄)) β (π« π΄ β π« π΄)) |
39 | 33, 37, 38 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
π« (π΄ Γ π΄)) β (π« π΄ β π« π΄)) |
40 | | gchdjuidm 10663 |
. . . . . . . . . . . . 13
β’
((π« π΄ β
GCH β§ Β¬ π« π΄
β Fin) β (π« π΄ β π« π΄) β π« π΄) |
41 | 2, 10, 40 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
π« π΄) β
π« π΄) |
42 | | entr 9002 |
. . . . . . . . . . . 12
β’
(((π« π΄
β π« (π΄
Γ π΄)) β
(π« π΄ β
π« π΄) β§
(π« π΄ β
π« π΄) β
π« π΄) β
(π« π΄ β
π« (π΄ Γ π΄)) β π« π΄) |
43 | 39, 41, 42 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
π« (π΄ Γ π΄)) β π« π΄) |
44 | | pwen 9150 |
. . . . . . . . . . 11
β’
((π« π΄
β π« (π΄
Γ π΄)) β
π« π΄ β
π« (π« π΄
β π« (π΄
Γ π΄)) β
π« π« π΄) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π« π΄
β π« (π΄
Γ π΄)) β
π« π« π΄) |
46 | | entr 9002 |
. . . . . . . . . 10
β’
(((π« π« π΄ Γ π« π« (π΄ Γ π΄)) β π« (π« π΄ β π« (π΄ Γ π΄)) β§ π« (π« π΄ β π« (π΄ Γ π΄)) β π« π« π΄) β (π« π«
π΄ Γ π«
π« (π΄ Γ π΄)) β π« π«
π΄) |
47 | 31, 45, 46 | syl2anc 585 |
. . . . . . . . 9
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π« π΄
Γ π« π« (π΄ Γ π΄)) β π« π« π΄) |
48 | | domentr 9009 |
. . . . . . . . 9
β’
(((π« π« π΄ Γ π« (harβπ΄)) βΌ (π« π«
π΄ Γ π«
π« (π΄ Γ π΄)) β§ (π« π«
π΄ Γ π«
π« (π΄ Γ π΄)) β π« π«
π΄) β (π«
π« π΄ Γ
π« (harβπ΄))
βΌ π« π« π΄) |
49 | 26, 47, 48 | syl2anc 585 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π« π΄
Γ π« (harβπ΄)) βΌ π« π« π΄) |
50 | | endomtr 9008 |
. . . . . . . 8
β’
((π« (π« π΄ β (harβπ΄)) β (π« π« π΄ Γ π«
(harβπ΄)) β§
(π« π« π΄
Γ π« (harβπ΄)) βΌ π« π« π΄) β π« (π«
π΄ β (harβπ΄)) βΌ π« π«
π΄) |
51 | 19, 49, 50 | syl2anc 585 |
. . . . . . 7
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π« π΄
β (harβπ΄))
βΌ π« π« π΄) |
52 | | sdomdomtr 9110 |
. . . . . . 7
β’
(((π« π΄
β (harβπ΄))
βΊ π« (π« π΄ β (harβπ΄)) β§ π« (π« π΄ β (harβπ΄)) βΌ π« π«
π΄) β (π« π΄ β (harβπ΄)) βΊ π« π«
π΄) |
53 | 17, 51, 52 | syl2anc 585 |
. . . . . 6
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
(harβπ΄)) βΊ
π« π« π΄) |
54 | | gchen1 10620 |
. . . . . 6
β’
(((π« π΄
β GCH β§ Β¬ π« π΄ β Fin) β§ (π« π΄ βΌ (π« π΄ β (harβπ΄)) β§ (π« π΄ β (harβπ΄)) βΊ π« π«
π΄)) β π« π΄ β (π« π΄ β (harβπ΄))) |
55 | 2, 10, 12, 53, 54 | syl22anc 838 |
. . . . 5
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π΄ β
(π« π΄ β
(harβπ΄))) |
56 | | djucomen 10172 |
. . . . . 6
β’
((π« π΄ β
GCH β§ (harβπ΄)
β V) β (π« π΄ β (harβπ΄)) β ((harβπ΄) β π« π΄)) |
57 | 2, 13, 56 | syl2anc 585 |
. . . . 5
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
(harβπ΄)) β
((harβπ΄) β
π« π΄)) |
58 | | entr 9002 |
. . . . 5
β’
((π« π΄
β (π« π΄
β (harβπ΄))
β§ (π« π΄ β
(harβπ΄)) β
((harβπ΄) β
π« π΄)) β
π« π΄ β
((harβπ΄) β
π« π΄)) |
59 | 55, 57, 58 | syl2anc 585 |
. . . 4
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π΄ β
((harβπ΄) β
π« π΄)) |
60 | 59 | ensymd 9001 |
. . 3
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
((harβπ΄) β
π« π΄) β
π« π΄) |
61 | | domentr 9009 |
. . 3
β’
(((harβπ΄)
βΌ ((harβπ΄)
β π« π΄) β§
((harβπ΄) β
π« π΄) β
π« π΄) β
(harβπ΄) βΌ
π« π΄) |
62 | 4, 60, 61 | syl2anc 585 |
. 2
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(harβπ΄) βΌ
π« π΄) |
63 | | gchdjuidm 10663 |
. . . . . 6
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β (π΄ β π΄) β π΄) |
64 | 21, 8, 63 | syl2anc 585 |
. . . . 5
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ β π΄) β π΄) |
65 | | pwen 9150 |
. . . . 5
β’ ((π΄ β π΄) β π΄ β π« (π΄ β π΄) β π« π΄) |
66 | 64, 65 | syl 17 |
. . . 4
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π΄ β π΄) β π« π΄) |
67 | | djudoml 10179 |
. . . . . . . 8
β’ ((π΄ β GCH β§
(harβπ΄) β On)
β π΄ βΌ (π΄ β (harβπ΄))) |
68 | 21, 1, 67 | sylancl 587 |
. . . . . . 7
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β π΄ βΌ (π΄ β (harβπ΄))) |
69 | | harndom 9557 |
. . . . . . . 8
β’ Β¬
(harβπ΄) βΌ π΄ |
70 | | djudoml 10179 |
. . . . . . . . . . 11
β’
(((harβπ΄)
β On β§ π΄ β
GCH) β (harβπ΄)
βΌ ((harβπ΄)
β π΄)) |
71 | 1, 21, 70 | sylancr 588 |
. . . . . . . . . 10
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(harβπ΄) βΌ
((harβπ΄) β
π΄)) |
72 | | djucomen 10172 |
. . . . . . . . . . 11
β’
(((harβπ΄)
β On β§ π΄ β
GCH) β ((harβπ΄)
β π΄) β (π΄ β (harβπ΄))) |
73 | 1, 21, 72 | sylancr 588 |
. . . . . . . . . 10
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
((harβπ΄) β
π΄) β (π΄ β (harβπ΄))) |
74 | | domentr 9009 |
. . . . . . . . . 10
β’
(((harβπ΄)
βΌ ((harβπ΄)
β π΄) β§
((harβπ΄) β
π΄) β (π΄ β (harβπ΄))) β (harβπ΄) βΌ (π΄ β (harβπ΄))) |
75 | 71, 73, 74 | syl2anc 585 |
. . . . . . . . 9
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(harβπ΄) βΌ
(π΄ β
(harβπ΄))) |
76 | | domen2 9120 |
. . . . . . . . 9
β’ (π΄ β (π΄ β (harβπ΄)) β ((harβπ΄) βΌ π΄ β (harβπ΄) βΌ (π΄ β (harβπ΄)))) |
77 | 75, 76 | syl5ibrcom 246 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ β (π΄ β (harβπ΄)) β (harβπ΄) βΌ π΄)) |
78 | 69, 77 | mtoi 198 |
. . . . . . 7
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β Β¬
π΄ β (π΄ β (harβπ΄))) |
79 | | brsdom 8971 |
. . . . . . 7
β’ (π΄ βΊ (π΄ β (harβπ΄)) β (π΄ βΌ (π΄ β (harβπ΄)) β§ Β¬ π΄ β (π΄ β (harβπ΄)))) |
80 | 68, 78, 79 | sylanbrc 584 |
. . . . . 6
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β π΄ βΊ (π΄ β (harβπ΄))) |
81 | | canth2g 9131 |
. . . . . . . . . 10
β’ (π΄ β GCH β π΄ βΊ π« π΄) |
82 | | sdomdom 8976 |
. . . . . . . . . 10
β’ (π΄ βΊ π« π΄ β π΄ βΌ π« π΄) |
83 | 21, 81, 82 | 3syl 18 |
. . . . . . . . 9
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β π΄ βΌ π« π΄) |
84 | | djudom1 10177 |
. . . . . . . . 9
β’ ((π΄ βΌ π« π΄ β§ (harβπ΄) β On) β (π΄ β (harβπ΄)) βΌ (π« π΄ β (harβπ΄))) |
85 | 83, 1, 84 | sylancl 587 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ β (harβπ΄)) βΌ (π« π΄ β (harβπ΄))) |
86 | | djudom2 10178 |
. . . . . . . . 9
β’
(((harβπ΄)
βΌ π« π΄ β§
π« π΄ β GCH)
β (π« π΄
β (harβπ΄))
βΌ (π« π΄
β π« π΄)) |
87 | 62, 2, 86 | syl2anc 585 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(π« π΄ β
(harβπ΄)) βΌ
(π« π΄ β
π« π΄)) |
88 | | domtr 9003 |
. . . . . . . 8
β’ (((π΄ β (harβπ΄)) βΌ (π« π΄ β (harβπ΄)) β§ (π« π΄ β (harβπ΄)) βΌ (π« π΄ β π« π΄)) β (π΄ β (harβπ΄)) βΌ (π« π΄ β π« π΄)) |
89 | 85, 87, 88 | syl2anc 585 |
. . . . . . 7
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ β (harβπ΄)) βΌ (π« π΄ β π« π΄)) |
90 | | domentr 9009 |
. . . . . . 7
β’ (((π΄ β (harβπ΄)) βΌ (π« π΄ β π« π΄) β§ (π« π΄ β π« π΄) β π« π΄) β (π΄ β (harβπ΄)) βΌ π« π΄) |
91 | 89, 41, 90 | syl2anc 585 |
. . . . . 6
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ β (harβπ΄)) βΌ π« π΄) |
92 | | gchen2 10621 |
. . . . . 6
β’ (((π΄ β GCH β§ Β¬ π΄ β Fin) β§ (π΄ βΊ (π΄ β (harβπ΄)) β§ (π΄ β (harβπ΄)) βΌ π« π΄)) β (π΄ β (harβπ΄)) β π« π΄) |
93 | 21, 8, 80, 91, 92 | syl22anc 838 |
. . . . 5
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β (π΄ β (harβπ΄)) β π« π΄) |
94 | 93 | ensymd 9001 |
. . . 4
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π΄ β (π΄ β (harβπ΄))) |
95 | | entr 9002 |
. . . 4
β’
((π« (π΄
β π΄) β
π« π΄ β§ π«
π΄ β (π΄ β (harβπ΄))) β π« (π΄ β π΄) β (π΄ β (harβπ΄))) |
96 | 66, 94, 95 | syl2anc 585 |
. . 3
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« (π΄ β π΄) β (π΄ β (harβπ΄))) |
97 | | endom 8975 |
. . 3
β’
(π« (π΄
β π΄) β (π΄ β (harβπ΄)) β π« (π΄ β π΄) βΌ (π΄ β (harβπ΄))) |
98 | | pwdjudom 10211 |
. . 3
β’
(π« (π΄
β π΄) βΌ (π΄ β (harβπ΄)) β π« π΄ βΌ (harβπ΄)) |
99 | 96, 97, 98 | 3syl 18 |
. 2
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
π« π΄ βΌ
(harβπ΄)) |
100 | | sbth 9093 |
. 2
β’
(((harβπ΄)
βΌ π« π΄ β§
π« π΄ βΌ
(harβπ΄)) β
(harβπ΄) β
π« π΄) |
101 | 62, 99, 100 | syl2anc 585 |
1
β’ ((Ο
βΌ π΄ β§ π΄ β GCH β§ π«
π΄ β GCH) β
(harβπ΄) β
π« π΄) |