Theorem xpdom2 4428

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

Hypotheses

Ref	Expression
xpdom.1	|- B e. V
xpdom.2	|- C e. V

Assertion

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

Proof of Theorem xpdom2

Step	Hyp	Ref	Expression
1		reldom 4361	. . 3 |- Rel ~<_
2	1	brrelexi 3203	. 2 |- (A ~<_ B -> A e. V)
3		breq1 2617	. . . 4 |- (t = A -> (t ~<_ B <-> A ~<_ B))
4		xpeq2 3196	. . . . 5 |- (t = A -> (C X. t) = (C X. A))
5	4	breq1d 2624	. . . 4 |- (t = A -> ((C X. t) ~<_ (C X. B) <-> (C X. A) ~<_ (C X. B)))
6	3, 5	imbi12d 625	. . 3 |- (t = A -> ((t ~<_ B -> (C X. t) ~<_ (C X. B)) <-> (A ~<_ B -> (C X. A) ~<_ (C X. B))))
7		xpdom.1	. . . . 5 |- B e. V
8	7	brdom 4366	. . . 4 |- (t ~<_ B <-> E.f f:t-1-1->B)
9		xpdom.2	. . . . . . 7 |- C e. V
10		visset 1809	. . . . . . 7 |- t e. V
11	9, 10	xpex 3255	. . . . . 6 |- (C X. t) e. V
12		f1f 3656	. . . . . . . . . . 11 |- (f:t-1-1->B -> f:t-->B)
13		ffvelrn 3805	. . . . . . . . . . . 12 |- ((f:t-->B /\ U.ran { x} e. t) -> (f` U.ran { x}) e. B)
14	13	ex 373	. . . . . . . . . . 11 |- (f:t-->B -> (U.ran { x} e. t -> (f` U.ran { x}) e. B))
15	12, 14	syl 10	. . . . . . . . . 10 |- (f:t-1-1->B -> (U.ran { x} e. t -> (f` U.ran { x}) e. B))
16	15	anim2d 560	. . . . . . . . 9 |- (f:t-1-1->B -> ((U.dom { x} e. C /\ U.ran { x} e. t) -> (U.dom { x} e. C /\ (f` U.ran { x}) e. B)))
17	16	adantld 390	. . . . . . . 8 |- (f:t-1-1->B -> ((x = <.U.dom { x}, U.ran { x}>. /\ (U.dom { x} e. C /\ U.ran { x} e. t)) -> (U.dom { x} e. C /\ (f` U.ran { x}) e. B)))
18		elxp4 3445	. . . . . . . 8 |- (x e. (C X. t) <-> (x = <.U.dom { x}, U.ran { x}>. /\ (U.dom { x} e. C /\ U.ran { x} e. t)))
19		fvex 3723	. . . . . . . . 9 |- (f` U.ran { x}) e. V
20	19	opelxp 3209	. . . . . . . 8 |- (<.U.dom { x}, (f` U.ran { x})>. e. (C X. B) <-> (U.dom { x} e. C /\ (f` U.ran { x}) e. B))
21	17, 18, 20	3imtr4g 552	. . . . . . 7 |- (f:t-1-1->B -> (x e. (C X. t) -> <.U.dom { x}, (f` U.ran { x})>. e. (C X. B)))
22		f1fveq 3867	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:t-1-1->B /\ (w e. t /\ u e. t)) -> ((f` w) = (f` u) <-> w = u))
23	22	ancoms 436	. . . . . . . . . . . . . . . . . . . . . 22 |- (((w e. t /\ u e. t) /\ f:t-1-1->B) -> ((f` w) = (f` u) <-> w = u))
24	23	anbi2d 615	. . . . . . . . . . . . . . . . . . . . 21 |- (((w e. t /\ u e. t) /\ f:t-1-1->B) -> ((z = v /\ (f` w) = (f` u)) <-> (z = v /\ w = u)))
25		visset 1809	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. V
26		fvex 3723	. . . . . . . . . . . . . . . . . . . . . 22 |- (f` w) e. V
27		fvex 3723	. . . . . . . . . . . . . . . . . . . . . 22 |- (f` u) e. V
28	25, 26, 27	opth 2782	. . . . . . . . . . . . . . . . . . . . 21 |- (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ (f` w) = (f` u)))
29	24, 28	syl5bb 531	. . . . . . . . . . . . . . . . . . . 20 |- (((w e. t /\ u e. t) /\ f:t-1-1->B) -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u)))
30	29	ex 373	. . . . . . . . . . . . . . . . . . 19 |- ((w e. t /\ u e. t) -> (f:t-1-1->B -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u))))
31	30	ad2ant2l 408	. . . . . . . . . . . . . . . . . 18 |- (((z e. C /\ w e. t) /\ (v e. C /\ u e. t)) -> (f:t-1-1->B -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u))))
32	31	imp 350	. . . . . . . . . . . . . . . . 17 |- ((((z e. C /\ w e. t) /\ (v e. C /\ u e. t)) /\ f:t-1-1->B) -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u)))
33	32	adantlr 393	. . . . . . . . . . . . . . . 16 |- (((((z e. C /\ w e. t) /\ (v e. C /\ u e. t)) /\ (x = <.z, w>. /\ y = <.v, u>.)) /\ f:t-1-1->B) -> (<.z, (f` w)>. = <.v, (f` u)>. <-> (z = v /\ w = u)))
34		sneq 2413	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = <.z, w>. -> {x} = {<.z, w>.})
35	34	dmeqd 3308	. . . . . . . . . . . . . . . . . . . . 21 |- (x = <.z, w>. -> dom { x} = dom {<.z, w>.})
36	35	unieqd 2507	. . . . . . . . . . . . . . . . . . . 20 |- (x = <.z, w>. -> U.dom { x} = U.dom {<.z, w>.})
37	25	op1sta 3440	. . . . . . . . . . . . . . . . . . . 20 |- U.dom {<.z, w>.} = z
38	36, 37	syl6eq 1520	. . . . . . . . . . . . . . . . . . 19 |- (x = <.z, w>. -> U.dom { x} = z)
39	34	rneqd 3336	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = <.z, w>. -> ran { x} = ran {<.z, w>.})
40	39	unieqd 2507	. . . . . . . . . . . . . . . . . . . . 21 |- (x = <.z, w>. -> U.ran { x} = U.ran {<.z, w>.})
41		visset 1809	. . . . . . . . . . . . . . . . . . . . . 22 |- w e. V
42	25, 41	op2nda 3444	. . . . . . . . . . . . . . . . . . . . 21 |- U.ran {<.z, w>.} = w
43	40, 42	syl6eq 1520	. . . . . . . . . . . . . . . . . . . 20 |- (x = <.z, w>. -> U.ran { x} = w)
44	43	fveq2d 3719	. . . . . . . . . . . . . . . . . . 19 |- (x = <.z, w>. -> (f` U.ran { x}) = (f` w))
45	38, 44	opeq12d 2491	. . . . . . . . . . . . . . . . . 18 |- (x = <.z, w>. -> <.U.dom { x}, (f` U.ran { x})>. = <.z, (f` w)>.)
46		sneq 2413	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.v, u>. -> {y} = {<.v, u>.})
47	46	dmeqd 3308	. . . . . . . . . . . . . . . . . . . . 21 |- (y = <.v, u>. -> dom { y} = dom {<.v, u>.})
48	47	unieqd 2507	. . . . . . . . . . . . . . . . . . . 20 |- (y = <.v, u>. -> U.dom { y} = U.dom {<.v, u>.})
49		visset 1809	. . . . . . . . . . . . . . . . . . . . 21 |- v e. V
50	49	op1sta 3440	. . . . . . . . . . . . . . . . . . . 20 |- U.dom {<.v, u>.} = v
51	48, 50	syl6eq 1520	. . . . . . . . . . . . . . . . . . 19 |- (y = <.v, u>. -> U.dom { y} = v)
52	46	rneqd 3336	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.v, u>. -> ran { y} = ran {<.v, u>.})
53	52	unieqd 2507	. . . . . . . . . . . . . . . . . . . . 21 |- (y = <.v, u>. -> U.ran { y} = U.ran {<.v, u>.})
54		visset 1809	. . . . . . . . . . . . . . . . . . . . . 22 |- u e. V
55	49, 54	op2nda 3444	. . . . . . . . . . . . . . . . . . . . 21 |- U.ran {<.v, u>.} = u
56	53, 55	syl6eq 1520	. . . . . . . . . . . . . . . . . . . 20 |- (y = <.v, u>. -> U.ran { y} = u)
57	56	fveq2d 3719	. . . . . . . . . . . . . . . . . . 19 |- (y = <.v, u>. -> (f` U.ran { y}) = (f` u))
58	51, 57	opeq12d 2491	. . . . . . . . . . . . . . . . . 18 |- (y = <.v, u>. -> <.U.dom { y}, (f` U.ran { y})>. = <.v, (f` u)>.)
59	45, 58	eqeqan12d 1487	. . . . . . . . . . . . . . . . 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)>.))
60	59	ad2antlr 405	. . . . . . . . . . . . . . . 16 |- (((((z e. C /\ w e. t) /\ (v e. C /\ u e. t)) /\ (x = <.z, w>. /\ y = <.v, u>.)) /\ f:t-1-1->B) -> (<.U.dom { x}, (f` U.ran { x})>. = <.U.dom { y}, (f` U.ran { y})>. <-> <.z, (f` w)>. = <.v, (f` u)>.))
61		eqeq12 1484	. . . . . . . . . . . . . . . . . 18 |- ((x = <.z, w>. /\ y = <.v, u>.) -> (x = y <-> <.z, w>. = <.v, u>.))
62	25, 41, 54	opth 2782	. . . . . . . . . . . . . . . . . 18 |- (<.z, w>. = <.v, u>. <-> (z = v /\ w = u))
63	61, 62	syl6bb 535	. . . . . . . . . . . . . . . . 17 |- ((x = <.z, w>. /\ y = <.v, u>.) -> (x = y <-> (z = v /\ w = u)))
64	63	ad2antlr 405	. . . . . . . . . . . . . . . 16 |- (((((z e. C /\ w e. t) /\ (v e. C /\ u e. t)) /\ (x = <.z, w>. /\ y = <.v, u>.)) /\ f:t-1-1->B) -> (x = y <-> (z = v /\ w = u)))
65	33, 60, 64	3bitr4d 549	. . . . . . . . . . . . . . 15 |- (((((z e. C /\ w e. t) /\ (v e. C /\ u e. t)) /\