Theorem unxpdomlem 3649

Description: Lemma for unxpdom 3650.

Hypotheses

Ref	Expression
unxpdomlem.1	|- A e. V
unxpdomlem.2	|- B e. V

Assertion

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

Proof of Theorem unxpdomlem

Step	Hyp	Ref	Expression
1		cleq1 1107	. . . . . . . . . . . . . . . . . . . . 21 |- (x = f -> (x = w <-> f = w))
2		ifbi 1783	. . . . . . . . . . . . . . . . . . . . 21 |- ((x = w <-> f = w) -> if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, x)))
3	1, 2	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (x = f -> if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, x)))
4		ifeq2 1779	. . . . . . . . . . . . . . . . . . . . 21 |- (x = f -> if(y = v, v, x) = if(y = v, v, f))
5		ifeq2 1779	. . . . . . . . . . . . . . . . . . . . 21 |- (if(y = v, v, x) = if(y = v, v, f) -> if(f = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, f)))
6	4, 5	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (x = f -> if(f = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, f)))
7	3, 6	eqtrd 1128	. . . . . . . . . . . . . . . . . . 19 |- (x = f -> if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, f)))
8	7	cleq1d 1109	. . . . . . . . . . . . . . . . . 18 |- (x = f -> (if(x = w, if(y = v, w, y), if(y = v, v, x)) = f <-> if(f = w, if(y = v, w, y), if(y = v, v, f)) = f))
9		ifeq12 1782	. . . . . . . . . . . . . . . . . . . 20 |- ((if(y = v, w, y) = if(v = v, w, v) /\ if(y = v, v, f) = if(v = v, v, f)) -> if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(v = v, w, v), if(v = v, v, f)))
10		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = v -> (y = v <-> v = v))
11		ifbi 1783	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y = v <-> v = v) -> if(y = v, w, y) = if(v = v, w, y))
12	10, 11	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (y = v -> if(y = v, w, y) = if(v = v, w, y))
13		ifeq2 1779	. . . . . . . . . . . . . . . . . . . . 21 |- (y = v -> if(v = v, w, y) = if(v = v, w, v))
14	12, 13	eqtrd 1128	. . . . . . . . . . . . . . . . . . . 20 |- (y = v -> if(y = v, w, y) = if(v = v, w, v))
15		ifbi 1783	. . . . . . . . . . . . . . . . . . . . 21 |- ((y = v <-> v = v) -> if(y = v, v, f) = if(v = v, v, f))
16	10, 15	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (y = v -> if(y = v, v, f) = if(v = v, v, f))
17	9, 14, 16	sylanc 361	. . . . . . . . . . . . . . . . . . 19 |- (y = v -> if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(v = v, w, v), if(v = v, v, f)))
18	17	cleq1d 1109	. . . . . . . . . . . . . . . . . 18 |- (y = v -> (if(f = w, if(y = v, w, y), if(y = v, v, f)) = f <-> if(f = w, if(v = v, w, v), if(v = v, v, f)) = f))
19	8, 18	rcla42ev 1405	. . . . . . . . . . . . . . . . 17 |- (((f e. A /\ v e. B) /\ if(f = w, if(v = v, w, v), if(v = v, v, f)) = f) -> E.x e. A E.y e. B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
20		iftrue 1780	. . . . . . . . . . . . . . . . . . 19 |- (f = w -> if(f = w, if(v = v, w, v), if(v = v, v, f)) = if(v = v, w, v))
21		cleqid 1102	. . . . . . . . . . . . . . . . . . . 20 |- v = v
22		iftrue 1780	. . . . . . . . . . . . . . . . . . . 20 |- (v = v -> if(v = v, w, v) = w)
23	21, 22	ax-mp 6	. . . . . . . . . . . . . . . . . . 19 |- if(v = v, w, v) = w
24	20, 23	syl6eq 1140	. . . . . . . . . . . . . . . . . 18 |- (f = w -> if(f = w, if(v = v, w, v), if(v = v, v, f)) = w)
25		id 9	. . . . . . . . . . . . . . . . . 18 |- (f = w -> f = w)
26	24, 25	eqtr4d 1131	. . . . . . . . . . . . . . . . 17 |- (f = w -> if(f = w, if(v = v, w, v), if(v = v, v, f)) = f)
27	19, 26	sylan2 346	. . . . . . . . . . . . . . . 16 |- (((f e. A /\ v e. B) /\ f = w) -> E.x e. A E.y e. B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
28	27	exp31 293	. . . . . . . . . . . . . . 15 |- (f e. A -> (v e. B -> (f = w -> E.x e. A E.y e. B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
29	28	com3l 34	. . . . . . . . . . . . . 14 |- (v e. B -> (f = w -> (f e. A -> E.x e. A E.y e. B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
30	29	ad2antlr 321	. . . . . . . . . . . . 13 |- (((t e. B /\ v e. B) /\ -. t = v) -> (f = w -> (f e. A -> E.x e. A E.y e. B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
31		ifeq12 1782	. . . . . . . . . . . . . . . . . . . . 21 |- ((if(y = v, w, y) = if(t = v, w, t) /\ if(y = v, v, f) = if(t = v, v, f)) -> if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(t = v, w, t), if(t = v, v, f)))
32		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = t -> (y = v <-> t = v))
33		ifbi 1783	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y = v <-> t = v) -> if(y = v, w, y) = if(t = v, w, y))
34	32, 33	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = t -> if(y = v, w, y) = if(t = v, w, y))
35		ifeq2 1779	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = t -> if(t = v, w, y) = if(t = v, w, t))
36	34, 35	eqtrd 1128	. . . . . . . . . . . . . . . . . . . . 21 |- (y = t -> if(y = v, w, y) = if(t = v, w, t))
37		ifbi 1783	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y = v <-> t = v) -> if(y = v, v, f) = if(t = v, v, f))
38	32, 37	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (y = t -> if(y = v, v, f) = if(t = v, v, f))
39	31, 36, 38	sylanc 361	. . . . . . . . . . . . . . . . . . . 20 |- (y = t -> if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(t = v, w, t), if(t = v, v, f)))
40	39	cleq1d 1109	. . . . . . . . . . . . . . . . . . 19 |- (y = t -> (if(f = w, if(y = v, w, y), if(y = v, v, f)) = f <-> if(f = w, if(t = v, w, t), if(t = v, v, f)) = f))
41	8, 40	rcla42ev 1405	. . . . . . . . . . . . . . . . . 18 |- (((f e. A /\ t e. B) /\ if(f = w, if(t = v, w, t), if(t = v, v, f)) = f) -> E.x e. A E.y e. B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
42		iffalse 1781	. . . . . . . . . . . . . . . . . . 19 |- (-. f = w -> if(f = w, if(t = v, w, t), if(t = v, v, f)) = if(t = v, v, f))
43		iffalse 1781	. . . . . . . . . . . . . . . . . . 19 |- (-. t = v -> if(t = v, v, f) = f)
44	42, 43	sylan9eqr 1145	. . . . . . . . . . . . . . . . . 18 |- ((-. t = v /\ -. f = w) -> if(f = w, if(t = v, w, t), if(t = v, v, f)) = f)
45	41, 44	sylan2 346	. . . . . . . . . . . . . . . . 17 |- (((f e. A /\ t e. B) /\ (-. t = v /\ -. f = w)) -> E.x e. A E.y e. B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
46	45	exp43 301	. . . . . . . . . . . . . . . 16 |- (f e. A -> (t e. B