Theorem ishomd 10689

Description: The predicate F e. ((hom` T)` <.A, B>.) JFM vol. 1.2 p. 411 th. 18.

Hypotheses

Ref	Expression
ishomd.1	|- O = dom (id` T)
ishomd.2	|- M = dom (dom` T)
ishomd.3	|- D = (dom` T)
ishomd.4	|- C = (cod` T)
ishomd.5	|- H = (hom` T)

Assertion

Ref	Expression
ishomd	|- ((T e. Cat /\ A e. O /\ B e. O) -> (F e. (H` <.A, B>.) <-> (F e. M /\ (D` F) = A /\ (C` F) = B)))

Proof of Theorem ishomd

Step	Hyp	Ref	Expression
1		fveq2 3730	. . . . . . . 8 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> (id` T) = (id` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)))
2	1	dmeqd 3319	. . . . . . 7 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> dom (id` T) = dom (id` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)))
3		ishomd.1	. . . . . . 7 |- O = dom (id` T)
4	2, 3	syl5eq 1522	. . . . . 6 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> O = dom (id` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)))
5	4	eleq2d 1544	. . . . 5 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> (A e. O <-> A e. dom (id` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.))))
6	4	eleq2d 1544	. . . . 5 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> (B e. O <-> B e. dom (id` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.))))
7	5, 6	anbi12d 630	. . . 4 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> ((A e. O /\ B e. O) <-> (A e. dom (id` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)) /\ B e. dom (id` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)))))
8		fveq2 3730	. . . . . . . 8 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> (hom` T) = (hom` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)))
9		ishomd.5	. . . . . . . 8 |- H = (hom` T)
10	8, 9	syl5eq 1522	. . . . . . 7 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> H = (hom` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)))
11	10	fveq1d 3732	. . . . . 6 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> (H` <.A, B>.) = ((hom` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.))` <.A, B>.))
12	11	eleq2d 1544	. . . . 5 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> (F e. (H` <.A, B>.) <-> F e. ((hom` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.))` <.A, B>.)))
13		fveq2 3730	. . . . . . . . 9 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> (dom` T) = (dom` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.)))
14	13	dmeqd 3319	. . . . . . . 8 |- (T = if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x>.>.}, {<.<.<.x, x>., <.x, x>.>., <.x, x>.>.}>.>.) -> dom (dom` T) = dom (dom` if(T e. Cat, T, <.<.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>., <.{<.x, <.x, x