Theorem unxpdom 4864

Description: Cross product dominates union for sets with cardinality greater than 1. Proposition 10.36 of [TakeutiZaring] p. 93.

Assertion

Ref	Expression
unxpdom	|- ((1o ~< A /\ 1o ~< B) -> (A u. B) ~<_ (A X. B))

Proof of Theorem unxpdom

Step	Hyp	Ref	Expression
1		sdomex 4492	. . . 4 |- (1o ~< A -> (1o e. V /\ A e. V))
2	1	pm3.27d 325	. . 3 |- (1o ~< A -> A e. V)
3		sdomex 4492	. . . 4 |- (1o ~< B -> (1o e. V /\ B e. V))
4	3	pm3.27d 325	. . 3 |- (1o ~< B -> B e. V)
5	2, 4	anim12i 333	. 2 |- ((1o ~< A /\ 1o ~< B) -> (A e. V /\ B e. V))
6		breq2 2638	. . . . 5 |- (x = A -> (1o ~< x <-> 1o ~< A))
7	6	anbi1d 620	. . . 4 |- (x = A -> ((1o ~< x /\ 1o ~< y) <-> (1o ~< A /\ 1o ~< y)))
8		uneq1 2188	. . . . 5 |- (x = A -> (x u. y) = (A u. y))
9		xpeq1 3216	. . . . 5 |- (x = A -> (x X. y) = (A X. y))
10	8, 9	breq12d 2646	. . . 4 |- (x = A -> ((x u. y) ~<_ (x X. y) <-> (A u. y) ~<_ (A X. y)))
11	7, 10	imbi12d 629	. . 3 |- (x = A -> (((1o ~< x /\ 1o ~< y) -> (x u. y) ~<_ (x X. y)) <-> ((1o ~< A /\ 1o ~< y) -> (A u. y) ~<_ (A X. y))))
12		breq2 2638	. . . . 5 |- (y = B -> (1o ~< y <-> 1o ~< B))
13	12	anbi2d 619	. . . 4 |- (y = B -> ((1o ~< A /\ 1o ~< y) <-> (1o ~< A /\ 1o ~< B)))
14		uneq2 2189	. . . . 5 |- (y = B -> (A u. y) = (A u. B))
15		xpeq2 3217	. . . . 5 |- (y = B -> (A X. y) = (A X. B))
16	14, 15	breq12d 2646	. . . 4 |- (y = B -> ((A u. y) ~<_ (A X. y) <-> (A u. B) ~<_ (A X. B)))
17	13, 16	imbi12d 629	. . 3 |- (y = B -> (((1o ~< A /\ 1o ~< y) -> (A u. y) ~<_ (A X. y)) <-> ((1o ~< A /\ 1o ~< B) -> (A u. B) ~<_ (A X. B))))
18		visset 1820	. . . 4 |- x e. V
19		visset 1820	. . . 4 |- y e. V
20	18, 19	unxpdomlem 4863	. . 3 |- ((1o ~< x /\ 1o ~< y) -> (x u. y) ~<_ (x X. y))
21	11, 17, 20	vtocl2g 1857	. 2 |- ((A e. V /\ B e. V) -> ((1o ~< A /\ 1o ~< B) -> (A u. B) ~<_ (A X. B)))
22	5, 21	mpcom 49	1 |- ((1o ~< A /\ 1o ~< B) -> (A u. B) ~<_ (A X. B))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 960   e. wcel 962  Vcvv 1818   u. cun 2056   class class class wbr 2634   X. cxp 3184  1oc1o 4144   ~<_ cdom 4383   ~< csdm 4384

This theorem is referenced by:  unxpdom2 4865  sucxpdom 4866  infxpidmlem1 7585

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-rep 2708  ax-sep 2718  ax-nul 2725  ax-pow 2758  ax-pr 2795  ax-un 2882  ax-inf2 4642  ax-ac 4761

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2012  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-pss 2066  df-nul 2292  df-if 2374  df-pw 2414  df-sn 2424  df-pr 2425  df-tp 2427  df-op 2428  df-uni 2518  df-int 2548  df-iun 2582  df-br 2635  df-opab 2682  df-tr 2696  df-eprel 2848  df-id 2851  df-po 2856  df-so 2866  df-fr 2933  df-we 2950  df-ord 2967  df-on 2968  df-lim 2969  df-suc 2970  df-om 3148  df-xp 3200  df-rel 3201  df-cnv 3202  df-co 3203  df-dm 3204  df-rn 3205  df-res 3206  df-ima 3207  df-fun 3208  df-fn 3209  df-f 3210  df-f1 3211  df-fo 3212  df-f1o 3213  df-fv 3214  df-rdg 3948  df-opr 3981  df-oprab 3982  df-1st 4095  df-2nd 4096  df-1o 4149  df-2o 4150  df-er 4277  df-en 4386  df-dom 4387  df-sdom 4388  df-fin 4389  df-card 4833

Copyright terms: Public domain