Theorem xpdom2 3345

Description: Dominance law for cross product. Proposition 10.33(2) of [TakeutiZaring] p. 92.

Hypotheses

Ref	Expression
xpdom2.1	|- A e. V
xpdom2.2	|- B e. V
xpdom2.3	|- C e. V

Assertion

Ref	Expression
xpdom2	|- (A ~<_ B -> (C X. A) ~<_ (C X. B))

Proof of Theorem xpdom2

Step	Hyp	Ref	Expression
1		xpdom2.2	. . 3 |- B e. V
2	1	brdom 3283	. 2 |- (A ~<_ B <-> E.f f:A-1-1->B)
3		xpdom2.3	. . . . 5 |- C e. V
4		xpdom2.1	. . . . 5 |- A e. V
5	3, 4	xpex 2488	. . . 4 |- (C X. A) e. V
6		f1f 2781	. . . . . . . . 9 |- (f:A-1-1->B -> f:A-->B)
7		ffvrn 2890	. . . . . . . . . 10 |- ((f:A-->B /\ U.ran {x} e. A) -> (f` U.ran {x}) e. B)
8	7	exp 291	. . . . . . . . 9 |- (f:A-->B -> (U.ran {x} e. A -> (f` U.ran {x}) e. B))
9	6, 8	syl 12	. . . . . . . 8 |- (f:A-1-1->B -> (U.ran {x} e. A -> (f` U.ran {x}) e. B))
10	9	anim2d 433	. . . . . . 7 |- (f:A-1-1->B -> ((U.dom {x} e. C /\ U.ran {x} e. A) -> (U.dom {x} e. C /\ (f` U.ran {x}) e. B)))
11	10	adantld 307	. . . . . 6 |- (f:A-1-1->B -> ((x = <.U.dom {x}, U.ran {x}>. /\ (U.dom {x} e. C /\ U.ran {x} e. A)) -> (U.dom {x} e. C /\ (f` U.ran {x}) e. B)))
12		elxp4 2640	. . . . . 6 |- (x e. (C X. A) <-> (x = <.U.dom {x}, U.ran {x}>. /\ (U.dom {x} e. C /\ U.ran {x} e. A)))
13		fvex 2838	. . . . . . 7 |- (f` U.ran {x}) e. V
14	13	opelxp 2452	. . . . . 6 |- (<.U.dom {x}, (f` U.ran {x})>. e. (C X. B) <-> (U.dom {x} e. C /\ (f` U.ran {x}) e. B))
15	11, 12, 14	3imtr4g 426	. . . . 5 |- (f:A-1-1->B -> (x e. (C X. A) -> <.U.dom {x}, (f` U.ran {x})>. e. (C X. B)))
16		sneq 1816	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = <.z, w>. -> {x} = {<.z, w>.})
17	16	dmeqd 2533	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = <.z, w>. -> dom {x} = dom {<.z, w>.})
18	17	unieqd 1929	. . . . . . . . . . . . . . . . . . . . 21 |- (x = <.z, w>. -> U.dom {x} = U.dom {<.z, w>.})
19		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. V
20	19	op1sta 2635	. . . . . . . . . . . . . . . . . . . . 21 |- U.dom {<.z, w>.} = z
21	18, 20	syl6eq 1140	. . . . . . . . . . . . . . . . . . . 20 |- (x = <.z, w>. -> U.dom {x} = z)
22	16	rneqd 2557	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = <.z, w>. -> ran {x} = ran {<.z, w>.})
23	22	unieqd 1929	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = <.z, w>. -> U.ran {x} = U.ran {<.z, w>.})
24		visset 1350	. . . . . . . . . . . . . . . . . . . . . . 23 |- w e. V
25	19, 24	op2nda 2639	. . . . . . . . . . . . . . . . . . . . . 22 |- U.ran {<.z, w>.} = w
26	23, 25	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . 21 |- (x = <.z, w>. -> U.ran {x} = w)
27	26	fveq2d 2836	. . . . . . . . . . . . . . . . . . . 20 |- (x = <.z, w>. -> (f` U.ran {x}) = (f` w))
28	21, 27	jca 236	. . . . . . . . . . . . . . . . . . 19 |- (x = <.z, w>. -> (U.dom {x} = z /\ (f` U.ran {x}) = (f` w)))
29		snex 1859	. . . . . . . . . . . . . . . . . . . . . 22 |- {x} e. V
30		dmexg 2551	. . . . . . . . . . . . . . . . . . . . . 22 |- ({x} e. V -> dom {x} e. V)
31	29, 30	ax-mp 6	. . . . . . . . . . . . . . . . . . . . 21 |- dom {x} e. V
32	31	uniex 1947	. . . . . . . . . . . . . . . . . . . 20 |- U.dom {x} e. V
33		fvex 2838	. . . . . . . . . . . . . . . . . . . 20 |- (f` w) e. V
34	32, 13, 33	opth 1898	. . . . . . . . . . . . . . . . . . 19 |- (<.U.dom {x}, (f` U.ran {x})>. = <.z, (f` w)>. <-> (U.dom {x} = z /\ (f` U.ran {x}) = (f` w)))
35	28, 34	sylibr 175	. . . . . . . . . . . . . . . . . 18 |- (x = <.z, w>. -> <.U.dom {x}, (f` U.ran {x})>. = <.z, (f` w)>.)
36		sneq 1816	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = <.v, u>. -> {y} = {<.v, u>.})
37	36	dmeqd 2533	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.v, u>. -> dom {y} = dom {<.v, u>.})
38	37	unieqd 1929	. . . . . . . . . . . . . . . . . . . . 21 |- (y = <.v, u>. -> U.dom {y} = U.dom {<.v, u>.})
39		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 |- v e. V
40	39	op1sta 2635	. . . . . . . . . . . . . . . . . . . . 21 |- U.dom {<.v, u>.} = v
41	38, 40	syl6eq 1140	. . . . . . . . . . . . . . . . . . . 20 |- (y = <.v, u>. -> U.dom {y} = v)
42	36	rneqd 2557	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = <.v, u>. -> ran {y} = ran {<.v, u>.})
43	42	unieqd 1929	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.v, u>. -> U.ran {y} = U.ran {<.v, u>.})
44		visset 1350	. . . . . . . . . . . . . . . . . . . . . . 23 |- u e. V
45	39, 44	op2nda 2639	. . . . . . . . . . . . . . . . . . . . . 22 |- U.ran {<.v, u>.} = u
46	43, 45	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . 21 |- (y = <.v, u>. -> U.ran {y} = u)
47	46	fveq2d 2836	. . . . . . . . . . . . . . . . . . . 20 |- (y = <.v, u>. -> (f` U.ran {y}) = (f` u))
48	41, 47	jca 236	. . . . . . . . . . . . . . . . . . 19 |- (y = <.v, u>. -> (U.dom {y} = v /\ (f` U.ran {y}) = (f` u)))
49		snex 1859	. . . . . . . . . . . . . . . . . . . . . 22 |- {y} e. V
50		dmexg 2551	. . . . . . . . . . . . . . . . . . . . . 22 |- ({y} e. V -> dom {y} e. V)
51	49, 50	ax-mp 6	. . . . . . . . . . . . . . . . . . . . 21 |- dom {y} e. V
52	51	uniex 1947	. . . . . . . . . . . . . . . . . . . 20 |- U.dom {y} e. V
53		fvex 2838	. . . . . . . . . . . . . . . . . . . 20 |- (f` U.ran {y}) e. V
54		fvex 2838	. . . . . . . . . . . . . . . . . . . 20 |- (f` u) e. V
55	52, 53, 54	opth 1898	. . . . . . . . . . . . . . . . . . 19 |- (<.U.dom {y}, (f` U.ran {y})>. = <.v, (f` u)>. <-> (U.dom {y} = v /\ (f` U.ran {y}) = (f` u)))
56	48, 55	sylibr 175	. . . . . . . . . . . . . . . . . 18 |- (y = <.v, u>. -> <.U.dom {y}, (f` U.ran {y})>. = <.v, (f` u)>.)
57	35, 56	cleqan12d 1116	. . . . . . . . . . . . . . . . 17 |- ((x = <.z, w>. /\ y = <.v, u>.) -> (<.U.dom {x}, (f` U.ran {x})>. = <.U.dom {y}, (f` U.ran {y})>. <-> <.z, (f` w)>. = <.v, (f` u)>.))
58	57	adantl 305	. . . . . . . . . . . . . . . 16 |- ((((z e. C /\ w e. A) /\ (v e. C /\ u e. A)) /\ (x = <.z, w>. /\ y = <.v, u>.)) -> (<.U.dom {x}, (f` U.ran {x})>. = <.U.dom {y}, (f` U.ran {y})>. <-> <.z, (f` w)>. = <.v, (f` u)>.))
59	58	adantr 306	. . . . . . . . . . . . . . 15 |- (((((z e. C /\ w e. A) /\ (v e. C /\ u e. A)) /\ (x = <.z, w>. /\ y = <.v, u>.)) /\ f:A-1-1->B) -> (<.U.dom {x}, (f` U.ran {x})>. = <.U.dom {y}, (f` U.ran {y})>. <-> <.z, (f` w)>. = <.v, (f` u)>.))
60		f1fveq 2918	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:A-1-1->B /\ (w e. A /\ u e. A)) -> ((f` w) = (f` u) <-> w = u))
61	60	ancoms 334	. . . . . . . . . . . . . . . . . . . . . 22 |- (((w e. A /\ u e. A) /\ f:A-1-1->B) -> ((f` w) = (f` u) <-> w = u))
62	61	anbi2d 468	. . . . . . . . . . . . . . . . . . . . 21 |- (((w e. A /\ u e. A) /\ f:A-1-1->B) -> ((z = v /\ (f` w) = (f` u)) <-> (z = v /\ w = u)))
63	19, 33, 54	opth 1898	. . . . . . . . . . . . . . . . . . . . 21 |- (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ (f` w) = (f` u)))
64	62, 63	syl5bb 410	. . . . . . . . . . . . . . . . . . . 20 |- (((w e. A /\ u e. A) /\ f:A-1-1->B) -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u)))
65	64	exp 291	. . . . . . . . . . . . . . . . . . 19 |- ((w e. A /\ u e. A) -> (f:A-1-1->B -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u))))
66	65	adantrl 311	. . . . . . . . . . . . . . . . . 18 |- ((w e. A /\ (v e. C /\ u e. A)) -> (f:A-1-1->B -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u))))
67	66	adantll 309	. . . . . . . . . . . . . . . . 17 |- (((z e. C /\ w e. A) /\ (v e. C /\ u e. A)) -> (f:A-1-1->B -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u))))
68	67	imp 277	. . . . . . . . . . . . . . . 16 |- ((((z e. C /\ w e. A) /\ (v e. C /\ u e. A)) /\ f:A-1-1->B) -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u)))
69	68	adantlr 310	. . . . . . . . . . . . . . 15 |- (((((z e. C /\ w e. A) /\ (v e. C /\ u e.