Step | Hyp | Ref
| Expression |
1 | | 2on 8427 |
. . 3
β’
2o β On |
2 | | eqid 2733 |
. . . 4
β’
(SetCatβ2o) =
(SetCatβ2o) |
3 | 2 | setccat 17976 |
. . 3
β’
(2o β On β (SetCatβ2o) β
Cat) |
4 | 1, 3 | ax-mp 5 |
. 2
β’
(SetCatβ2o) β Cat |
5 | 1 | a1i 11 |
. . . 4
β’ (β€
β 2o β On) |
6 | | eqid 2733 |
. . . 4
β’
(Baseβ(SetCatβ2o)) =
(Baseβ(SetCatβ2o)) |
7 | | eqid 2733 |
. . . 4
β’ (Hom
β(SetCatβ2o)) = (Hom
β(SetCatβ2o)) |
8 | | 0ex 5265 |
. . . . . . 7
β’ β
β V |
9 | 8 | prid1 4724 |
. . . . . 6
β’ β
β {β
, {β
}} |
10 | | df2o2 8422 |
. . . . . 6
β’
2o = {β
, {β
}} |
11 | 9, 10 | eleqtrri 2833 |
. . . . 5
β’ β
β 2o |
12 | 11 | a1i 11 |
. . . 4
β’ (β€
β β
β 2o) |
13 | | p0ex 5340 |
. . . . . . 7
β’ {β
}
β V |
14 | 13 | prid2 4725 |
. . . . . 6
β’ {β
}
β {β
, {β
}} |
15 | 14, 10 | eleqtrri 2833 |
. . . . 5
β’ {β
}
β 2o |
16 | 15 | a1i 11 |
. . . 4
β’ (β€
β {β
} β 2o) |
17 | | 0nep0 5314 |
. . . . 5
β’ β
β {β
} |
18 | 17 | a1i 11 |
. . . 4
β’ (β€
β β
β {β
}) |
19 | 2, 5, 6, 7, 12, 16, 18 | cat1lem 17987 |
. . 3
β’ (β€
β βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€))) |
20 | 19 | mptru 1549 |
. 2
β’
βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) |
21 | | fvexd 6858 |
. . . 4
β’ (π = (SetCatβ2o)
β (Baseβπ)
β V) |
22 | | fveq2 6843 |
. . . 4
β’ (π = (SetCatβ2o)
β (Baseβπ) =
(Baseβ(SetCatβ2o))) |
23 | | fvexd 6858 |
. . . . 5
β’ ((π = (SetCatβ2o)
β§ π =
(Baseβ(SetCatβ2o))) β (Hom βπ) β V) |
24 | | fveq2 6843 |
. . . . . 6
β’ (π = (SetCatβ2o)
β (Hom βπ) =
(Hom β(SetCatβ2o))) |
25 | 24 | adantr 482 |
. . . . 5
β’ ((π = (SetCatβ2o)
β§ π =
(Baseβ(SetCatβ2o))) β (Hom βπ) = (Hom
β(SetCatβ2o))) |
26 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (β = (Hom
β(SetCatβ2o)) β (π₯βπ¦) = (π₯(Hom
β(SetCatβ2o))π¦)) |
27 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (β = (Hom
β(SetCatβ2o)) β (π§βπ€) = (π§(Hom
β(SetCatβ2o))π€)) |
28 | 26, 27 | ineq12d 4174 |
. . . . . . . . . . 11
β’ (β = (Hom
β(SetCatβ2o)) β ((π₯βπ¦) β© (π§βπ€)) = ((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€))) |
29 | 28 | neeq1d 3000 |
. . . . . . . . . 10
β’ (β = (Hom
β(SetCatβ2o)) β (((π₯βπ¦) β© (π§βπ€)) β β
β ((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
)) |
30 | 29 | anbi1d 631 |
. . . . . . . . 9
β’ (β = (Hom
β(SetCatβ2o)) β ((((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
31 | 30 | 2rexbidv 3210 |
. . . . . . . 8
β’ (β = (Hom
β(SetCatβ2o)) β (βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ§ β π βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
32 | 31 | 2rexbidv 3210 |
. . . . . . 7
β’ (β = (Hom
β(SetCatβ2o)) β (βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
33 | 32 | adantl 483 |
. . . . . 6
β’ (((π = (SetCatβ2o)
β§ π =
(Baseβ(SetCatβ2o))) β§ β = (Hom β(SetCatβ2o)))
β (βπ₯ β
π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
34 | | pm4.61 406 |
. . . . . . . . . . 11
β’ (Β¬
(((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) β (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€))) |
35 | 34 | 2rexbii 3125 |
. . . . . . . . . 10
β’
(βπ§ β
π βπ€ β π Β¬ (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) β βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€))) |
36 | | rexnal2 3129 |
. . . . . . . . . 10
β’
(βπ§ β
π βπ€ β π Β¬ (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) β Β¬ βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€))) |
37 | 35, 36 | bitr3i 277 |
. . . . . . . . 9
β’
(βπ§ β
π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β Β¬ βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€))) |
38 | 37 | 2rexbii 3125 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β π βπ¦ β π Β¬ βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€))) |
39 | | rexnal2 3129 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π Β¬ βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) β Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€))) |
40 | 38, 39 | bitri 275 |
. . . . . . 7
β’
(βπ₯ β
π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€))) |
41 | 40 | a1i 11 |
. . . . . 6
β’ (((π = (SetCatβ2o)
β§ π =
(Baseβ(SetCatβ2o))) β§ β = (Hom β(SetCatβ2o)))
β (βπ₯ β
π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)))) |
42 | | rexeq 3309 |
. . . . . . . . . 10
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
43 | 42 | 2rexbidv 3210 |
. . . . . . . . 9
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ¦ β π βπ§ β π βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ¦ β π βπ§ β π βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
44 | 43 | rexbidv 3172 |
. . . . . . . 8
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β π βπ¦ β π βπ§ β π βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
45 | | rexeq 3309 |
. . . . . . . . 9
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ§ β π βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
46 | 45 | 2rexbidv 3210 |
. . . . . . . 8
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ₯ β π βπ¦ β π βπ§ β π βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β π βπ¦ β π βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
47 | | rexeq 3309 |
. . . . . . . . 9
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ¦ β π βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
48 | 47 | rexeqbi1dv 3307 |
. . . . . . . 8
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ₯ β π βπ¦ β π βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
49 | 44, 46, 48 | 3bitrd 305 |
. . . . . . 7
β’ (π =
(Baseβ(SetCatβ2o)) β (βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
50 | 49 | ad2antlr 726 |
. . . . . 6
β’ (((π = (SetCatβ2o)
β§ π =
(Baseβ(SetCatβ2o))) β§ β = (Hom β(SetCatβ2o)))
β (βπ₯ β
π βπ¦ β π βπ§ β π βπ€ β π (((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)) β βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
51 | 33, 41, 50 | 3bitr3d 309 |
. . . . 5
β’ (((π = (SetCatβ2o)
β§ π =
(Baseβ(SetCatβ2o))) β§ β = (Hom β(SetCatβ2o)))
β (Β¬ βπ₯
β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) β βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
52 | 23, 25, 51 | sbcied2 3787 |
. . . 4
β’ ((π = (SetCatβ2o)
β§ π =
(Baseβ(SetCatβ2o))) β ([(Hom βπ) / β] Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) β βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
53 | 21, 22, 52 | sbcied2 3787 |
. . 3
β’ (π = (SetCatβ2o)
β ([(Baseβπ) / π][(Hom βπ) / β] Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) β βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€)))) |
54 | 53 | rspcev 3580 |
. 2
β’
(((SetCatβ2o) β Cat β§ βπ₯ β
(Baseβ(SetCatβ2o))βπ¦ β
(Baseβ(SetCatβ2o))βπ§ β
(Baseβ(SetCatβ2o))βπ€ β
(Baseβ(SetCatβ2o))(((π₯(Hom
β(SetCatβ2o))π¦) β© (π§(Hom
β(SetCatβ2o))π€)) β β
β§ Β¬ (π₯ = π§ β§ π¦ = π€))) β βπ β Cat [(Baseβπ) / π][(Hom βπ) / β] Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€))) |
55 | 4, 20, 54 | mp2an 691 |
1
β’
βπ β Cat
[(Baseβπ) /
π][(Hom
βπ) / β] Β¬ βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (((π₯βπ¦) β© (π§βπ€)) β β
β (π₯ = π§ β§ π¦ = π€)) |