Theorem 1ded 10753

Description: Category 1 is a deductive system. We can think of the morphism of Category 1 as corresponding to ph|- ph.

Hypothesis

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

Assertion

Ref	Expression
1ded	|- <.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Ded

Proof of Theorem 1ded

Step	Hyp	Ref	Expression
1		snex 2806	. . . 4 |- {<.<.A, A>., A>.} e. V
2		snex 2806	. . . 4 |- {<.A, <.A, A>.>.} e. V
3	1, 1, 2	3pm3.2i 830	. . 3 |- ({<.<.A, A>., A>.} e. V /\ {<.<.A, A>., A>.} e. V /\ {<.A, <.A, A>.>.} e. V)
4		snex 2806	. . 3 |- {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} e. V
5		dmsnop 3385	. . . . 5 |- dom {<.<.A, A>., A>.} = {<.A, A>.}
6	5	eqcomi 1526	. . . 4 |- {<.A, A>.} = dom {<.<.A, A>., A>.}
7		dmsnop 3385	. . . . 5 |- dom {<.A, <.A, A>.>.} = {A}
8	7	eqcomi 1526	. . . 4 |- {A} = dom {<.A, <.A, A>.>.}
9	6, 8	isded 10751	. . 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. Ded <-> ((<.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Alg /\ A.z e. {A} (({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z /\ ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z) /\ A.x e. {<.A, A>.}A.y e. {<.A, A>.} (<.y, x>. e. dom {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} <-> ({<.<.A, A>., A>.}` y) = ({<.<.A, A>., A>.}` x))) /\ (A.x e. {<.A, A>.}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = ({<.<.A, A>., A>.}` x) -> ({<.<.A, A>., A>.}` (y{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}x)) = ({<.<.A, A>., A>.}` x)) /\ A.x e. {<.A, A>.}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = ({<.<.A, A>., A>.}` x) -> ({<.<.A, A>., A>.}` (y{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}x)) = ({<.<.A, A>., A>.}` y))))))
10	3, 4, 9	mp2an 709	. 2 |- (<.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Ded <-> ((<.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Alg /\ A.z e. {A} (({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z /\ ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z) /\ A.x e. {<.A, A>.}A.y e. {<.A, A>.} (<.y, x>. e. dom {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.} <-> ({<.<.A, A>., A>.}` y) = ({<.<.A, A>., A>.}` x))) /\ (A.x e. {<.A, A>.}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = ({<.<.A, A>., A>.}` x) -> ({<.<.A, A>., A>.}` (y{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}x)) = ({<.<.A, A>., A>.}` x)) /\ A.x e. {<.A, A>.}A.y e. {<.A, A>.} (({<.<.A, A>., A>.}` y) = ({<.<.A, A>., A>.}` x) -> ({<.<.A, A>., A>.}` (y{<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}x)) = ({<.<.A, A>., A>.}` y)))))
11		1ded.1	. . . 4 |- A e. V
12	11	1alg 10736	. . 3 |- <.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Alg
13		elsni 2484	. . . . . 6 |- (z e. {A} -> z = A)
14		opex 2838	. . . . . . . . . 10 |- <.A, A>. e. V
15	11, 14	fvsn 3851	. . . . . . . . 9 |- ({<.A, <.A, A>.>.}` A) = <.A, A>.
16	15	fveq2i 3784	. . . . . . . 8 |- ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` A)) = ({<.<.A, A>., A>.}` <.A, A>.)
17	14, 11	fvsn 3851	. . . . . . . 8 |- ({<.<.A, A>., A>.}` <.A, A>.) = A
18	16, 17	eqtri 1542	. . . . . . 7 |- ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` A)) = A
19		fveq2 3781	. . . . . . . 8 |- (z = A -> ({<.A, <.A, A>.>.}` z) = ({<.A, <.A, A>.>.}` A))
20	19	fveq2d 3785	. . . . . . 7 |- (z = A -> ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` A)))
21		id 59	. . . . . . 7 |- (z = A -> z = A)
22	18, 20, 21	3eqtr4a 1579	. . . . . 6 |- (z = A -> ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z)
23	13, 22	syl 10	. . . . 5 |- (z e. {A} -> ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z)
24		anidmdbi 445	. . . . 5 |- ((z e. {A} -> (({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z /\ ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z)) <-> (z e. {A} -> ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z))
25	23, 24	mpbir 197	. . . 4 |- (z e. {A} -> (({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z /\ ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z))
26	25	rgen 1745	. . 3 |- A.z e. {A} (({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z /\ ({<.<.A, A>., A>.}` ({<.A, <.A, A>.>.}` z)) = z)
27		opex 2838	. . . . . . . . . 10 |- <.<.A, A>., <.A, A>.>. e. V
28	27	snid 2487	. . . . . . . . 9 |- <.<.A, A>., <.A, A>.>. e. {<.<.A, A>., <.A,