Step | Hyp | Ref
| Expression |
1 | | anass 470 |
. 2
β’ ((((π΄ β β*
β§ π΅ β
β*) β§ πΆ β β*) β§ (π΄π
πΆ β§ πΆππ΅)) β ((π΄ β β* β§ π΅ β β*)
β§ (πΆ β
β* β§ (π΄π
πΆ β§ πΆππ΅)))) |
2 | | df-3an 1090 |
. . 3
β’ ((π΄ β β*
β§ π΅ β
β* β§ πΆ
β β*) β ((π΄ β β* β§ π΅ β β*)
β§ πΆ β
β*)) |
3 | 2 | anbi1i 625 |
. 2
β’ (((π΄ β β*
β§ π΅ β
β* β§ πΆ
β β*) β§ (π΄π
πΆ β§ πΆππ΅)) β (((π΄ β β* β§ π΅ β β*)
β§ πΆ β
β*) β§ (π΄π
πΆ β§ πΆππ΅))) |
4 | | ixx.1 |
. . . . 5
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) |
5 | 4 | elixx1 13274 |
. . . 4
β’ ((π΄ β β*
β§ π΅ β
β*) β (πΆ β (π΄ππ΅) β (πΆ β β* β§ π΄π
πΆ β§ πΆππ΅))) |
6 | | 3anass 1096 |
. . . . 5
β’ ((πΆ β β*
β§ π΄π
πΆ β§ πΆππ΅) β (πΆ β β* β§ (π΄π
πΆ β§ πΆππ΅))) |
7 | | ibar 530 |
. . . . 5
β’ ((π΄ β β*
β§ π΅ β
β*) β ((πΆ β β* β§ (π΄π
πΆ β§ πΆππ΅)) β ((π΄ β β* β§ π΅ β β*)
β§ (πΆ β
β* β§ (π΄π
πΆ β§ πΆππ΅))))) |
8 | 6, 7 | bitrid 283 |
. . . 4
β’ ((π΄ β β*
β§ π΅ β
β*) β ((πΆ β β* β§ π΄π
πΆ β§ πΆππ΅) β ((π΄ β β* β§ π΅ β β*)
β§ (πΆ β
β* β§ (π΄π
πΆ β§ πΆππ΅))))) |
9 | 5, 8 | bitrd 279 |
. . 3
β’ ((π΄ β β*
β§ π΅ β
β*) β (πΆ β (π΄ππ΅) β ((π΄ β β* β§ π΅ β β*)
β§ (πΆ β
β* β§ (π΄π
πΆ β§ πΆππ΅))))) |
10 | 4 | ixxf 13275 |
. . . . . . 7
β’ π:(β* Γ
β*)βΆπ« β* |
11 | 10 | fdmi 6681 |
. . . . . 6
β’ dom π = (β* Γ
β*) |
12 | 11 | ndmov 7539 |
. . . . 5
β’ (Β¬
(π΄ β
β* β§ π΅
β β*) β (π΄ππ΅) = β
) |
13 | 12 | eleq2d 2824 |
. . . 4
β’ (Β¬
(π΄ β
β* β§ π΅
β β*) β (πΆ β (π΄ππ΅) β πΆ β β
)) |
14 | | noel 4291 |
. . . . . 6
β’ Β¬
πΆ β
β
|
15 | 14 | pm2.21i 119 |
. . . . 5
β’ (πΆ β β
β (π΄ β β*
β§ π΅ β
β*)) |
16 | | simpl 484 |
. . . . 5
β’ (((π΄ β β*
β§ π΅ β
β*) β§ (πΆ β β* β§ (π΄π
πΆ β§ πΆππ΅))) β (π΄ β β* β§ π΅ β
β*)) |
17 | 15, 16 | pm5.21ni 379 |
. . . 4
β’ (Β¬
(π΄ β
β* β§ π΅
β β*) β (πΆ β β
β ((π΄ β β* β§ π΅ β β*)
β§ (πΆ β
β* β§ (π΄π
πΆ β§ πΆππ΅))))) |
18 | 13, 17 | bitrd 279 |
. . 3
β’ (Β¬
(π΄ β
β* β§ π΅
β β*) β (πΆ β (π΄ππ΅) β ((π΄ β β* β§ π΅ β β*)
β§ (πΆ β
β* β§ (π΄π
πΆ β§ πΆππ΅))))) |
19 | 9, 18 | pm2.61i 182 |
. 2
β’ (πΆ β (π΄ππ΅) β ((π΄ β β* β§ π΅ β β*)
β§ (πΆ β
β* β§ (π΄π
πΆ β§ πΆππ΅)))) |
20 | 1, 3, 19 | 3bitr4ri 304 |
1
β’ (πΆ β (π΄ππ΅) β ((π΄ β β* β§ π΅ β β*
β§ πΆ β
β*) β§ (π΄π
πΆ β§ πΆππ΅))) |