Step | Hyp | Ref
| Expression |
1 | | gchaclem.4 |
. . . 4
β’ (π β (π΄ βΌ πΆ β§ (π΅ βΌ π« πΆ β π« π΄ βΌ π΅))) |
2 | 1 | simpld 496 |
. . 3
β’ (π β π΄ βΌ πΆ) |
3 | | reldom 8895 |
. . . . . 6
β’ Rel
βΌ |
4 | 3 | brrelex2i 5693 |
. . . . 5
β’ (π΄ βΌ πΆ β πΆ β V) |
5 | 2, 4 | syl 17 |
. . . 4
β’ (π β πΆ β V) |
6 | | canth2g 9081 |
. . . 4
β’ (πΆ β V β πΆ βΊ π« πΆ) |
7 | | sdomdom 8926 |
. . . 4
β’ (πΆ βΊ π« πΆ β πΆ βΌ π« πΆ) |
8 | 5, 6, 7 | 3syl 18 |
. . 3
β’ (π β πΆ βΌ π« πΆ) |
9 | | domtr 8953 |
. . 3
β’ ((π΄ βΌ πΆ β§ πΆ βΌ π« πΆ) β π΄ βΌ π« πΆ) |
10 | 2, 8, 9 | syl2anc 585 |
. 2
β’ (π β π΄ βΌ π« πΆ) |
11 | | gchaclem.3 |
. . . . . 6
β’ (π β π« πΆ β GCH) |
12 | 11 | adantr 482 |
. . . . 5
β’ ((π β§ π΅ βΌ π« π« πΆ) β π« πΆ β GCH) |
13 | | gchaclem.1 |
. . . . . . . 8
β’ (π β Ο βΌ π΄) |
14 | | domtr 8953 |
. . . . . . . 8
β’ ((Ο
βΌ π΄ β§ π΄ βΌ πΆ) β Ο βΌ πΆ) |
15 | 13, 2, 14 | syl2anc 585 |
. . . . . . 7
β’ (π β Ο βΌ πΆ) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π β§ π΅ βΌ π« π« πΆ) β Ο βΌ πΆ) |
17 | | pwdjuidm 10135 |
. . . . . 6
β’ (Ο
βΌ πΆ β (π«
πΆ β π« πΆ) β π« πΆ) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ ((π β§ π΅ βΌ π« π« πΆ) β (π« πΆ β π« πΆ) β π« πΆ) |
19 | | simpr 486 |
. . . . 5
β’ ((π β§ π΅ βΌ π« π« πΆ) β π΅ βΌ π« π« πΆ) |
20 | | gchdomtri 10573 |
. . . . 5
β’
((π« πΆ β
GCH β§ (π« πΆ
β π« πΆ)
β π« πΆ β§
π΅ βΌ π«
π« πΆ) β
(π« πΆ βΌ π΅ β¨ π΅ βΌ π« πΆ)) |
21 | 12, 18, 19, 20 | syl3anc 1372 |
. . . 4
β’ ((π β§ π΅ βΌ π« π« πΆ) β (π« πΆ βΌ π΅ β¨ π΅ βΌ π« πΆ)) |
22 | 21 | ex 414 |
. . 3
β’ (π β (π΅ βΌ π« π« πΆ β (π« πΆ βΌ π΅ β¨ π΅ βΌ π« πΆ))) |
23 | | pwdom 9079 |
. . . . 5
β’ (π΄ βΌ πΆ β π« π΄ βΌ π« πΆ) |
24 | | domtr 8953 |
. . . . . 6
β’
((π« π΄
βΌ π« πΆ β§
π« πΆ βΌ π΅) β π« π΄ βΌ π΅) |
25 | 24 | ex 414 |
. . . . 5
β’
(π« π΄ βΌ
π« πΆ β
(π« πΆ βΌ π΅ β π« π΄ βΌ π΅)) |
26 | 2, 23, 25 | 3syl 18 |
. . . 4
β’ (π β (π« πΆ βΌ π΅ β π« π΄ βΌ π΅)) |
27 | 1 | simprd 497 |
. . . 4
β’ (π β (π΅ βΌ π« πΆ β π« π΄ βΌ π΅)) |
28 | 26, 27 | jaod 858 |
. . 3
β’ (π β ((π« πΆ βΌ π΅ β¨ π΅ βΌ π« πΆ) β π« π΄ βΌ π΅)) |
29 | 22, 28 | syld 47 |
. 2
β’ (π β (π΅ βΌ π« π« πΆ β π« π΄ βΌ π΅)) |
30 | 10, 29 | jca 513 |
1
β’ (π β (π΄ βΌ π« πΆ β§ (π΅ βΌ π« π« πΆ β π« π΄ βΌ π΅))) |