Theorem 1cat 10536

Description: Category 1. A category with one object and one morphism.

Hypothesis

Ref	Expression
1cat.1	|- A e. V

Assertion

Ref	Expression
1cat	|- <.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Cat

Proof of Theorem 1cat

Step	Hyp	Ref	Expression
1		snex 2740	. . . 4 |- {<.<.A, A>., A>.} e. V
2		snex 2740	. . . 4 |- {<.A, <.A, A>.>.} e. V
3	1, 1, 2	3pm3.2i 816	. . 3 |- ({<.<.A, A>., A>.} e. V /\ {<.<.A, A>., A>.} e. V /\ {<.A, <.A, A>.>.} e. V)
4		snex 2740	. . 3 |- {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} e. V
5		dmsnop 3317	. . . . 5 |- dom {<.<.A, A>., A>.} = {<.A, A>.}
6	5	eqcomi 1471	. . . 4 |- {<.A, A>.} = dom {<.<.A, A>., A>.}
7		dmsnop 3317	. . . . 5 |- dom {<.A, <.A, A>.>.} = {A}
8	7	eqcomi 1471	. . . 4 |- {A} = dom {<.A, <.A, A>.>.}
9	6, 8	iscat 10531	. . 3 |- ((({<.<.A, A>., A>.} e. V /\ {<.<.A, A>., A>.} e. V /\ {<.A, <.A, A>.>.} e. V) /\ {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} e. V) -> (<.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Cat <-> ((<.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Ded /\ A.y e. {<.A, A>.}A.z e. {<.A, A>.}A.u e. {<.A, A>.} ((({<.<.A, A>., A>.}` u) = ({<.<.A, A>., A>.}` z) /\ ({<.<.A, A>., A>.}` z) = ({<.<.A, A>., A>.}` y)) -> (u{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} (z{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y)) = ((u{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}z){<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y))) /\ (A.x e. {A}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = x -> (({<.A, <.A, A>.>.}` x){<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y) = y) /\ A.x e. {A}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = x -> (y{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} ({<.A, <.A, A>.>.}` x)) = y)))))
10	3, 4, 9	mp2an 695	. 2 |- (<.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Cat <-> ((<.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Ded /\ A.y e. {<.A, A>.}A.z e. {<.A, A>.}A.u e. {<.A, A>.} ((({<.<.A, A>., A>.}` u) = ({<.<.A, A>., A>.}` z) /\ ({<.<.A, A>., A>.}` z) = ({<.<.A, A>., A>.}` y)) -> (u{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} (z{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y)) = ((u{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}z){<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y))) /\ (A.x e. {A}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = x -> (({<.A, <.A, A>.>.}` x){<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y) = y) /\ A.x e. {A}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = x -> (y{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} ({<.A, <.A, A>.>.}` x)) = y))))
11		1cat.1	. . . 4 |- A e. V
12	11	1ded 10515	. . 3 |- <.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Ded
13		id 59	. . . . . . . . . 10 |- (u = <.A, A>. -> u = <.A, A>.)
14	13	eqcomd 1472	. . . . . . . . 9 |- (u = <.A, A>. -> <.A, A>. = u)
15	14	3ad2ant3 800	. . . . . . . 8 |- ((y = <.A, A>. /\ z = <.A, A>. /\ u = <.A, A>.) -> <.A, A>. = u)
16		id 59	. . . . . . . . . . 11 |- (z = <.A, A>. -> z = <.A, A>.)
17	16	eqcomd 1472	. . . . . . . . . 10 |- (z = <.A, A>. -> <.A, A>. = z)
18	17	3ad2ant2 799	. . . . . . . . 9 |- ((y = <.A, A>. /\ z = <.A, A>. /\ u = <.A, A>.) -> <.A, A>. = z)
19		id 59	. . . . . . . . . . 11 |- (y = <.A, A>. -> y = <.A, A>.)
20	19	eqcomd 1472	. . . . . . . . . 10 |- (y = <.A, A>. -> <.A, A>. = y)
21	20	3ad2ant1 798	. . . . . . . . 9 |- ((y = <.A, A>. /\ z = <.A, A>. /\ u = <.A, A>.) -> <.A, A>. = y)
22	18, 21	opreq12d 3963	. . . . . . . 8 |- ((y = <.A, A>. /\ z = <.A, A>. /\ u = <.A, A>.) -> (<.A, A>.{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.) = (z{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y))
23	15, 22	opreq12d 3963	. . . . . . 7 |- ((y = <.A, A>. /\ z = <.A, A>. /\ u = <.A, A>.) -> (<.A, A>.{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} (<.A, A>.{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.)) = (u{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} (z{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}y)))
24	14	opreq1d 3960	. . . . . . . . . 10 |- (u = <.A, A>. -> (<.A, A>.{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.) = (u{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.))
25	24	opreq1d 3960	. . . . . . . . 9 |- (u = <.A, A>. -> ((<.A, A>.{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.){<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.) = ((u{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.){<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}<.A, A>.))
26	25	3ad2ant3 800	. . . . . . . 8 |- ((y = <.A, A>. /\ z