Step | Hyp | Ref
| Expression |
1 | | cat1lem.5 |
. . 3
β’ (π β β
β π) |
2 | | cat1lem.1 |
. . . . 5
β’ πΆ = (SetCatβπ) |
3 | | cat1lem.2 |
. . . . 5
β’ (π β π β π) |
4 | 2, 3 | setcbas 17964 |
. . . 4
β’ (π β π = (BaseβπΆ)) |
5 | | cat1lem.3 |
. . . 4
β’ π΅ = (BaseβπΆ) |
6 | 4, 5 | eqtr4di 2794 |
. . 3
β’ (π β π = π΅) |
7 | 1, 6 | eleqtrd 2839 |
. 2
β’ (π β β
β π΅) |
8 | | cat1lem.6 |
. . . 4
β’ (π β π β π) |
9 | 8, 6 | eleqtrd 2839 |
. . 3
β’ (π β π β π΅) |
10 | | f0 6723 |
. . . . 5
β’
β
:β
βΆβ
|
11 | | cat1lem.4 |
. . . . . 6
β’ π» = (Hom βπΆ) |
12 | 2, 3, 11, 1, 1 | elsetchom 17967 |
. . . . 5
β’ (π β (β
β
(β
π»β
) β
β
:β
βΆβ
)) |
13 | 10, 12 | mpbiri 257 |
. . . 4
β’ (π β β
β
(β
π»β
)) |
14 | | f0 6723 |
. . . . 5
β’
β
:β
βΆπ |
15 | 2, 3, 11, 1, 8 | elsetchom 17967 |
. . . . 5
β’ (π β (β
β
(β
π»π) β β
:β
βΆπ)) |
16 | 14, 15 | mpbiri 257 |
. . . 4
β’ (π β β
β
(β
π»π)) |
17 | | inelcm 4424 |
. . . 4
β’ ((β
β (β
π»β
)
β§ β
β (β
π»π)) β ((β
π»β
) β© (β
π»π)) β β
) |
18 | 13, 16, 17 | syl2anc 584 |
. . 3
β’ (π β ((β
π»β
) β© (β
π»π)) β β
) |
19 | | cat1lem.7 |
. . . . 5
β’ (π β β
β π) |
20 | 19 | neneqd 2948 |
. . . 4
β’ (π β Β¬ β
= π) |
21 | 20 | intnand 489 |
. . 3
β’ (π β Β¬ (β
= β
β§ β
= π)) |
22 | | oveq1 7364 |
. . . . . . 7
β’ (π§ = β
β (π§π»π€) = (β
π»π€)) |
23 | 22 | ineq2d 4172 |
. . . . . 6
β’ (π§ = β
β ((β
π»β
) β© (π§π»π€)) = ((β
π»β
) β© (β
π»π€))) |
24 | 23 | neeq1d 3003 |
. . . . 5
β’ (π§ = β
β
(((β
π»β
) β©
(π§π»π€)) β β
β ((β
π»β
) β© (β
π»π€)) β β
)) |
25 | | eqeq2 2748 |
. . . . . . 7
β’ (π§ = β
β (β
=
π§ β β
=
β
)) |
26 | 25 | anbi1d 630 |
. . . . . 6
β’ (π§ = β
β ((β
=
π§ β§ β
= π€) β (β
= β
β§ β
= π€))) |
27 | 26 | notbid 317 |
. . . . 5
β’ (π§ = β
β (Β¬
(β
= π§ β§ β
= π€) β Β¬ (β
= β
β§ β
= π€))) |
28 | 24, 27 | anbi12d 631 |
. . . 4
β’ (π§ = β
β
((((β
π»β
) β©
(π§π»π€)) β β
β§ Β¬ (β
= π§ β§ β
= π€)) β (((β
π»β
) β© (β
π»π€)) β β
β§ Β¬ (β
=
β
β§ β
= π€)))) |
29 | | oveq2 7365 |
. . . . . . 7
β’ (π€ = π β (β
π»π€) = (β
π»π)) |
30 | 29 | ineq2d 4172 |
. . . . . 6
β’ (π€ = π β ((β
π»β
) β© (β
π»π€)) = ((β
π»β
) β© (β
π»π))) |
31 | 30 | neeq1d 3003 |
. . . . 5
β’ (π€ = π β (((β
π»β
) β© (β
π»π€)) β β
β ((β
π»β
) β© (β
π»π)) β β
)) |
32 | | eqeq2 2748 |
. . . . . . 7
β’ (π€ = π β (β
= π€ β β
= π)) |
33 | 32 | anbi2d 629 |
. . . . . 6
β’ (π€ = π β ((β
= β
β§ β
=
π€) β (β
=
β
β§ β
= π))) |
34 | 33 | notbid 317 |
. . . . 5
β’ (π€ = π β (Β¬ (β
= β
β§
β
= π€) β Β¬
(β
= β
β§ β
= π))) |
35 | 31, 34 | anbi12d 631 |
. . . 4
β’ (π€ = π β ((((β
π»β
) β© (β
π»π€)) β β
β§ Β¬ (β
=
β
β§ β
= π€))
β (((β
π»β
)
β© (β
π»π)) β β
β§ Β¬
(β
= β
β§ β
= π)))) |
36 | 28, 35 | rspc2ev 3592 |
. . 3
β’ ((β
β π΅ β§ π β π΅ β§ (((β
π»β
) β© (β
π»π)) β β
β§ Β¬ (β
=
β
β§ β
= π))) β βπ§ β π΅ βπ€ β π΅ (((β
π»β
) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ β
= π€))) |
37 | 7, 9, 18, 21, 36 | syl112anc 1374 |
. 2
β’ (π β βπ§ β π΅ βπ€ β π΅ (((β
π»β
) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ β
= π€))) |
38 | | oveq1 7364 |
. . . . . . 7
β’ (π₯ = β
β (π₯π»π¦) = (β
π»π¦)) |
39 | 38 | ineq1d 4171 |
. . . . . 6
β’ (π₯ = β
β ((π₯π»π¦) β© (π§π»π€)) = ((β
π»π¦) β© (π§π»π€))) |
40 | 39 | neeq1d 3003 |
. . . . 5
β’ (π₯ = β
β (((π₯π»π¦) β© (π§π»π€)) β β
β ((β
π»π¦) β© (π§π»π€)) β β
)) |
41 | | eqeq1 2740 |
. . . . . . 7
β’ (π₯ = β
β (π₯ = π§ β β
= π§)) |
42 | 41 | anbi1d 630 |
. . . . . 6
β’ (π₯ = β
β ((π₯ = π§ β§ π¦ = π€) β (β
= π§ β§ π¦ = π€))) |
43 | 42 | notbid 317 |
. . . . 5
β’ (π₯ = β
β (Β¬ (π₯ = π§ β§ π¦ = π€) β Β¬ (β
= π§ β§ π¦ = π€))) |
44 | 40, 43 | anbi12d 631 |
. . . 4
β’ (π₯ = β
β ((((π₯π»π¦) β© (π§π»π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β (((β
π»π¦) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ π¦ = π€)))) |
45 | 44 | 2rexbidv 3213 |
. . 3
β’ (π₯ = β
β (βπ§ β π΅ βπ€ β π΅ (((π₯π»π¦) β© (π§π»π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ§ β π΅ βπ€ β π΅ (((β
π»π¦) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ π¦ = π€)))) |
46 | | oveq2 7365 |
. . . . . . 7
β’ (π¦ = β
β (β
π»π¦) = (β
π»β
)) |
47 | 46 | ineq1d 4171 |
. . . . . 6
β’ (π¦ = β
β ((β
π»π¦) β© (π§π»π€)) = ((β
π»β
) β© (π§π»π€))) |
48 | 47 | neeq1d 3003 |
. . . . 5
β’ (π¦ = β
β
(((β
π»π¦) β© (π§π»π€)) β β
β ((β
π»β
) β© (π§π»π€)) β β
)) |
49 | | eqeq1 2740 |
. . . . . . 7
β’ (π¦ = β
β (π¦ = π€ β β
= π€)) |
50 | 49 | anbi2d 629 |
. . . . . 6
β’ (π¦ = β
β ((β
=
π§ β§ π¦ = π€) β (β
= π§ β§ β
= π€))) |
51 | 50 | notbid 317 |
. . . . 5
β’ (π¦ = β
β (Β¬
(β
= π§ β§ π¦ = π€) β Β¬ (β
= π§ β§ β
= π€))) |
52 | 48, 51 | anbi12d 631 |
. . . 4
β’ (π¦ = β
β
((((β
π»π¦) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ π¦ = π€)) β (((β
π»β
) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ β
= π€)))) |
53 | 52 | 2rexbidv 3213 |
. . 3
β’ (π¦ = β
β (βπ§ β π΅ βπ€ β π΅ (((β
π»π¦) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ π¦ = π€)) β βπ§ β π΅ βπ€ β π΅ (((β
π»β
) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ β
= π€)))) |
54 | 45, 53 | rspc2ev 3592 |
. 2
β’ ((β
β π΅ β§ β
β π΅ β§ βπ§ β π΅ βπ€ β π΅ (((β
π»β
) β© (π§π»π€)) β β
β§ Β¬ (β
= π§ β§ β
= π€))) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ βπ€ β π΅ (((π₯π»π¦) β© (π§π»π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€))) |
55 | 7, 7, 37, 54 | syl3anc 1371 |
1
β’ (π β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ βπ€ β π΅ (((π₯π»π¦) β© (π§π»π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€))) |