Theorem unxpdomlem 4863

Description: Lemma for unxpdom 4864.

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		eqeq1 1488	. . . . . . . . . . . . . . . . . . . . 21 |- (x = f -> (x = w <-> f = w))
2	1	ifbid 2384	. . . . . . . . . . . . . . . . . . . 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)))
3		ifeq2 2377	. . . . . . . . . . . . . . . . . . . . 21 |- (x = f -> if(y = v, v, x) = if(y = v, v, f))
4	3	ifeq2d 2382	. . . . . . . . . . . . . . . . . . . 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)))
5	2, 4	eqtrd 1514	. . . . . . . . . . . . . . . . . . 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)))
6	5	eqeq1d 1490	. . . . . . . . . . . . . . . . . 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))
7		ifeq12 2380	. . . . . . . . . . . . . . . . . . . 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)))
8		eqeq1 1488	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = v -> (y = v <-> v = v))
9	8	ifbid 2384	. . . . . . . . . . . . . . . . . . . . 21 |- (y = v -> if(y = v, w, y) = if(v = v, w, y))
10		ifeq2 2377	. . . . . . . . . . . . . . . . . . . . 21 |- (y = v -> if(v = v, w, y) = if(v = v, w, v))
11	9, 10	eqtrd 1514	. . . . . . . . . . . . . . . . . . . 20 |- (y = v -> if(y = v, w, y) = if(v = v, w, v))
12	8	ifbid 2384	. . . . . . . . . . . . . . . . . . . 20 |- (y = v -> if(y = v, v, f) = if(v = v, v, f))
13	7, 11, 12	sylanc 474	. . . . . . . . . . . . . . . . . . 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)))
14	13	eqeq1d 1490	. . . . . . . . . . . . . . . . . 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))
15	6, 14	rcla42ev 1888	. . . . . . . . . . . . . . . . 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)
16		eqid 1482	. . . . . . . . . . . . . . . . . . 19 |- v = v
17		iftrue 2378	. . . . . . . . . . . . . . . . . . 19 |- (v = v -> if(v = v, w, v) = w)
18	16, 17	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- if(v = v, w, v) = w
19		iftrue 2378	. . . . . . . . . . . . . . . . . 18 |- (f = w -> if(f = w, if(v = v, w, v), if(v = v, v, f)) = if(v = v, w, v))
20		id 59	. . . . . . . . . . . . . . . . . 18 |- (f = w -> f = w)
21	18, 19, 20	3eqtr4a 1539	. . . . . . . . . . . . . . . . 17 |- (f = w -> if(f = w, if(v = v, w, v), if(v = v, v, f)) = f)
22	15, 21	syl3an3 865	. . . . . . . . . . . . . . . 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)
23	22	3exp 836	. . . . . . . . . . . . . . 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)))
24	23	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)))
25	24	ad2antlr 407	. . . . . . . . . . . . 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)))
26		ifeq12 2380	. . . . . . . . . . . . . . . . . . . . . 22 |- ((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)))
27		eqeq1 1488	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = t -> (y = v <-> t = v))
28	27	ifbid 2384	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = t -> if(y = v, w, y) = if(t = v, w, y))
29		ifeq2 2377	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = t -> if(t = v, w, y) = if(t = v, w, t))
30	28, 29	eqtrd 1514	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = t -> if(y = v, w, y) = if(t = v, w, t))
31	27	ifbid 2384	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = t -> if(y = v, v, f) = if(t = v, v, f))
32	26, 30, 31	sylanc 474	. . . . . . . . . . . . . . . . . . . . 21 |- (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)))
33	32	eqeq1d 1490	. . . . . . . . . . . . . . . . . . . 20 |- (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))
34	6, 33	rcla42ev 1888	. . . . . . . . . . . . . . . . . . 19 |- ((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)
35		iffalse 2379	. . . . . . . . . . . . . . . . . . . 20 |- (-. f = w -> if(f = w, if(t = v, w, t), if(t = v, v, f)) = if(t = v, v, f))
36		iffalse 2379	. . . . . . . . . . . . . . . . . . . 20 |- (-. t = v -> if(t = v, v, f) = f)
37	35, 36	sylan9eqr 1536	. . . . . . . . . . . . . . . . . . 19 |- ((-. t = v /\ -. f = w) -> if(f = w, if(t = v, w, t), if(t = v, v, f)) = f)
38	34, 37	syl3an3 865	. . . . . . . . . . . . . . . . . 18 |- ((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)
39	38	3exp 836	. . . . . . . . . . . . . . . . 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)))
40	39	exp4a 380	. . . . . . . . . . . . . . . 16 |- (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))))
41	40	imp3a 361	. . . . . . . . . . . . . . 15 |- (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)))
42	41	com3l 34	. . . . . . . . . . . . . 14 |- ((t 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)))
43	42	adantlr 395	. . . . . . . . . . . . 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,