Step | Hyp | Ref
| Expression |
1 | | mgcoval.1 |
. . . . 5
β’ π΄ = (Baseβπ) |
2 | | mgcoval.2 |
. . . . 5
β’ π΅ = (Baseβπ) |
3 | | mgcoval.3 |
. . . . 5
β’ β€ =
(leβπ) |
4 | | mgcoval.4 |
. . . . 5
β’ β² =
(leβπ) |
5 | | mgcval.1 |
. . . . 5
β’ π» = (πMGalConnπ) |
6 | | mgcval.2 |
. . . . 5
β’ (π β π β Proset ) |
7 | | mgcval.3 |
. . . . 5
β’ (π β π β Proset ) |
8 | 1, 2, 3, 4, 5, 6, 7 | mgcval 31896 |
. . . 4
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))))) |
9 | 8 | simprbda 500 |
. . 3
β’ ((π β§ πΉπ»πΊ) β (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) |
10 | 6 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β π β Proset ) |
11 | 7 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β π β Proset ) |
12 | | simp-4r 783 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β πΉπ»πΊ) |
13 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β π₯ β π΄) |
14 | | simplr 768 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β π¦ β π΄) |
15 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β π₯ β€ π¦) |
16 | 1, 2, 3, 4, 5, 10,
11, 12, 13, 14, 15 | mgcmnt1 31901 |
. . . . . . . 8
β’
(((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β (πΉβπ₯) β² (πΉβπ¦)) |
17 | 16 | ex 414 |
. . . . . . 7
β’ ((((π β§ πΉπ»πΊ) β§ π₯ β π΄) β§ π¦ β π΄) β (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
18 | 17 | anasss 468 |
. . . . . 6
β’ (((π β§ πΉπ»πΊ) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
19 | 18 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ πΉπ»πΊ) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
20 | 6 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β§ π’ β² π£) β π β Proset ) |
21 | 7 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β§ π’ β² π£) β π β Proset ) |
22 | | simp-4r 783 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β§ π’ β² π£) β πΉπ»πΊ) |
23 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β§ π’ β² π£) β π’ β π΅) |
24 | | simplr 768 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β§ π’ β² π£) β π£ β π΅) |
25 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β§ π’ β² π£) β π’ β² π£) |
26 | 1, 2, 3, 4, 5, 20,
21, 22, 23, 24, 25 | mgcmnt2 31902 |
. . . . . . . 8
β’
(((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β§ π’ β² π£) β (πΊβπ’) β€ (πΊβπ£)) |
27 | 26 | ex 414 |
. . . . . . 7
β’ ((((π β§ πΉπ»πΊ) β§ π’ β π΅) β§ π£ β π΅) β (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) |
28 | 27 | anasss 468 |
. . . . . 6
β’ (((π β§ πΉπ»πΊ) β§ (π’ β π΅ β§ π£ β π΅)) β (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) |
29 | 28 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ πΉπ»πΊ) β βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) |
30 | 19, 29 | jca 513 |
. . . 4
β’ ((π β§ πΉπ»πΊ) β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) |
31 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π’ β π΅) β π β Proset ) |
32 | 7 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π’ β π΅) β π β Proset ) |
33 | | simplr 768 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π’ β π΅) β πΉπ»πΊ) |
34 | | simpr 486 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π’ β π΅) β π’ β π΅) |
35 | 1, 2, 3, 4, 5, 31,
32, 33, 34 | mgccole2 31900 |
. . . . . 6
β’ (((π β§ πΉπ»πΊ) β§ π’ β π΅) β (πΉβ(πΊβπ’)) β² π’) |
36 | 35 | ralrimiva 3140 |
. . . . 5
β’ ((π β§ πΉπ»πΊ) β βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) |
37 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π₯ β π΄) β π β Proset ) |
38 | 7 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π₯ β π΄) β π β Proset ) |
39 | | simplr 768 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π₯ β π΄) β πΉπ»πΊ) |
40 | | simpr 486 |
. . . . . . 7
β’ (((π β§ πΉπ»πΊ) β§ π₯ β π΄) β π₯ β π΄) |
41 | 1, 2, 3, 4, 5, 37,
38, 39, 40 | mgccole1 31899 |
. . . . . 6
β’ (((π β§ πΉπ»πΊ) β§ π₯ β π΄) β π₯ β€ (πΊβ(πΉβπ₯))) |
42 | 41 | ralrimiva 3140 |
. . . . 5
β’ ((π β§ πΉπ»πΊ) β βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) |
43 | 36, 42 | jca 513 |
. . . 4
β’ ((π β§ πΉπ»πΊ) β (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯)))) |
44 | 30, 43 | jca 513 |
. . 3
β’ ((π β§ πΉπ»πΊ) β ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))) |
45 | 9, 44 | jca 513 |
. 2
β’ ((π β§ πΉπ»πΊ) β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯)))))) |
46 | 6 | ad4antr 731 |
. . . . . 6
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β π β Proset ) |
47 | 7 | ad4antr 731 |
. . . . . 6
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β π β Proset ) |
48 | | simp-4r 783 |
. . . . . . 7
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) |
49 | 48 | simpld 496 |
. . . . . 6
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β πΉ:π΄βΆπ΅) |
50 | 48 | simprd 497 |
. . . . . 6
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β πΊ:π΅βΆπ΄) |
51 | | simpllr 775 |
. . . . . . . 8
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) |
52 | 51 | simpld 496 |
. . . . . . 7
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
53 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β€ π¦ β π β€ π¦)) |
54 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
55 | 54 | breq1d 5116 |
. . . . . . . . 9
β’ (π₯ = π β ((πΉβπ₯) β² (πΉβπ¦) β (πΉβπ) β² (πΉβπ¦))) |
56 | 53, 55 | imbi12d 345 |
. . . . . . . 8
β’ (π₯ = π β ((π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β (π β€ π¦ β (πΉβπ) β² (πΉβπ¦)))) |
57 | | breq2 5110 |
. . . . . . . . 9
β’ (π¦ = π β (π β€ π¦ β π β€ π)) |
58 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
59 | 58 | breq2d 5118 |
. . . . . . . . 9
β’ (π¦ = π β ((πΉβπ) β² (πΉβπ¦) β (πΉβπ) β² (πΉβπ))) |
60 | 57, 59 | imbi12d 345 |
. . . . . . . 8
β’ (π¦ = π β ((π β€ π¦ β (πΉβπ) β² (πΉβπ¦)) β (π β€ π β (πΉβπ) β² (πΉβπ)))) |
61 | 56, 60 | cbvral2vw 3226 |
. . . . . . 7
β’
(βπ₯ β
π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β βπ β π΄ βπ β π΄ (π β€ π β (πΉβπ) β² (πΉβπ))) |
62 | 52, 61 | sylib 217 |
. . . . . 6
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β βπ β π΄ βπ β π΄ (π β€ π β (πΉβπ) β² (πΉβπ))) |
63 | 51 | simprd 497 |
. . . . . . 7
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) |
64 | | breq1 5109 |
. . . . . . . . 9
β’ (π’ = π β (π’ β² π£ β π β² π£)) |
65 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π’ = π β (πΊβπ’) = (πΊβπ)) |
66 | 65 | breq1d 5116 |
. . . . . . . . 9
β’ (π’ = π β ((πΊβπ’) β€ (πΊβπ£) β (πΊβπ) β€ (πΊβπ£))) |
67 | 64, 66 | imbi12d 345 |
. . . . . . . 8
β’ (π’ = π β ((π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)) β (π β² π£ β (πΊβπ) β€ (πΊβπ£)))) |
68 | | breq2 5110 |
. . . . . . . . 9
β’ (π£ = π β (π β² π£ β π β² π)) |
69 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π£ = π β (πΊβπ£) = (πΊβπ)) |
70 | 69 | breq2d 5118 |
. . . . . . . . 9
β’ (π£ = π β ((πΊβπ) β€ (πΊβπ£) β (πΊβπ) β€ (πΊβπ))) |
71 | 68, 70 | imbi12d 345 |
. . . . . . . 8
β’ (π£ = π β ((π β² π£ β (πΊβπ) β€ (πΊβπ£)) β (π β² π β (πΊβπ) β€ (πΊβπ)))) |
72 | 67, 71 | cbvral2vw 3226 |
. . . . . . 7
β’
(βπ’ β
π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)) β βπ β π΅ βπ β π΅ (π β² π β (πΊβπ) β€ (πΊβπ))) |
73 | 63, 72 | sylib 217 |
. . . . . 6
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β βπ β π΅ βπ β π΅ (π β² π β (πΊβπ) β€ (πΊβπ))) |
74 | | id 22 |
. . . . . . . 8
β’ (π₯ = π β π₯ = π) |
75 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π₯ = π β (πΊβ(πΉβπ₯)) = (πΊβ(πΉβπ))) |
76 | 74, 75 | breq12d 5119 |
. . . . . . 7
β’ (π₯ = π β (π₯ β€ (πΊβ(πΉβπ₯)) β π β€ (πΊβ(πΉβπ)))) |
77 | | simplr 768 |
. . . . . . 7
β’
((((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β§ π β π΄) β βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) |
78 | | simpr 486 |
. . . . . . 7
β’
((((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β§ π β π΄) β π β π΄) |
79 | 76, 77, 78 | rspcdva 3581 |
. . . . . 6
β’
((((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β§ π β π΄) β π β€ (πΊβ(πΉβπ))) |
80 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π’ = π β (πΉβ(πΊβπ’)) = (πΉβ(πΊβπ))) |
81 | | id 22 |
. . . . . . . 8
β’ (π’ = π β π’ = π) |
82 | 80, 81 | breq12d 5119 |
. . . . . . 7
β’ (π’ = π β ((πΉβ(πΊβπ’)) β² π’ β (πΉβ(πΊβπ)) β² π)) |
83 | | simpllr 775 |
. . . . . . 7
β’
((((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β§ π β π΅) β βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) |
84 | | simpr 486 |
. . . . . . 7
β’
((((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β§ π β π΅) β π β π΅) |
85 | 82, 83, 84 | rspcdva 3581 |
. . . . . 6
β’
((((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β§ π β π΅) β (πΉβ(πΊβπ)) β² π) |
86 | 1, 2, 3, 4, 5, 46,
47, 49, 50, 62, 73, 79, 85 | dfmgc2lem 31904 |
. . . . 5
β’
(((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) β πΉπ»πΊ) |
87 | 86 | anasss 468 |
. . . 4
β’ ((((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯)))) β πΉπ»πΊ) |
88 | 87 | anasss 468 |
. . 3
β’ (((π β§ (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))) β πΉπ»πΊ) |
89 | 88 | anasss 468 |
. 2
β’ ((π β§ ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯)))))) β πΉπ»πΊ) |
90 | 45, 89 | impbida 800 |
1
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))))) |