Theorem uninqs 14340

Description: Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 3197.

Hypothesis

Ref	Expression
uninqs.1	|- Er R

Assertion

Ref	Expression
uninqs	|- ((B C_ (A/.R) /\ C C_ (A/.R)) -> U.(B i^i C) = (U.B i^i U.C))

Proof of Theorem uninqs

Step	Hyp	Ref	Expression
1		dfss2 2610	. . . . . . . . . . . . . . 15 |- (B C_ (A/.R) <-> A.b(b e. B -> b e. (A/.R)))
2		dfss2 2610	. . . . . . . . . . . . . . . . . 18 |- (C C_ (A/.R) <-> A.a(a e. C -> a e. (A/.R)))
3		pm3.35 386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((a e. C /\ (a e. C -> a e. (A/.R))) -> a e. (A/.R))
4		pm3.35 386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((b e. B /\ (b e. B -> b e. (A/.R))) -> b e. (A/.R))
5		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- b e. _V
6	5	elqs 5348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (b e. (A/.R) <-> E.u e. A b = [u]R)
7		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- a e. _V
8	7	elqs 5348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (a e. (A/.R) <-> E.v e. A a = [v]R)
9		inelcm 2928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- ((x e. [v]R /\ x e. [u]R) -> ([v]R i^i [u]R) =/= (/))
10		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 |- (([v]R i^i [u]R) =/= (/) <-> -. ([v]R i^i [u]R) = (/))
11		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- v e. _V
12		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- u e. _V
13		uninqs.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- Er R
14	11, 12, 13	erdisj 5344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 |- ([v]R = [u]R \/ ([v]R i^i [u]R) = (/))
15		pm5.61 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- ((([v]R = [u]R \/ ([v]R i^i [u]R) = (/)) /\ -. ([v]R i^i [u]R) = (/)) <-> ([v]R = [u]R /\ -. ([v]R i^i [u]R) = (/)))
16		eqeq12 1896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 |- ((a = [v]R /\ b = [u]R) -> (a = b <-> [v]R = [u]R))
17	16	biimprcd 173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 |- ([v]R = [u]R -> ((a = [v]R /\ b = [u]R) -> a = b))
18	17	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- (([v]R = [u]R /\ -. ([v]R i^i [u]R) = (/)) -> ((a = [v]R /\ b = [u]R) -> a = b))
19	15, 18	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 |- ((([v]R = [u]R \/ ([v]R i^i [u]R) = (/)) /\ -. ([v]R i^i [u]R) = (/)) -> ((a = [v]R /\ b = [u]R) -> a = b))
20	14, 19	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 |- (-. ([v]R i^i [u]R) = (/) -> ((a = [v]R /\ b = [u]R) -> a = b))
21	10, 20	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- (([v]R i^i [u]R) =/= (/) -> ((a = [v]R /\ b = [u]R) -> a = b))
22	9, 21	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 |- ((x e. [v]R /\ x e. [u]R) -> ((a = [v]R /\ b = [u]R) -> a = b))
23		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- (a = [v]R -> (x e. a <-> x e. [v]R))
24	23	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 |- ((a = [v]R /\ x e. a) -> x e. [v]R)
25		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- (b = [u]R -> (x e. b <-> x e. [u]R))
26	25	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 |- ((b = [u]R /\ x e. b) -> x e. [u]R)
27	22, 24, 26	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 |- (((a = [v]R /\ x e. a) /\ (b = [u]R /\ x e. b)) -> ((a = [v]R /\ b = [u]R) -> a = b))
28	27	an4s 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 |- (((a = [v]R /\ b = [u]R) /\ (x e. a /\ x e. b)) -> ((a = [v]R /\ b = [u]R) -> a = b))
29	28	exp32 408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 |- ((a = [v]R /\ b = [u]R) -> (x e. a -> (x e. b -> ((a = [v]R /\ b = [u]R) -> a = b))))
30	29	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 |- ((a = [v]R /\ b = [u]R) -> ((a = [v]R /\ b = [u]R) -> (x e. b -> (x e. a -> a = b))))
31	30	pm2.43i 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 |- ((a = [v]R /\ b = [u]R) -> (x e. b -> (x e. a -> a = b)))
32	31	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 |- (a = [v]R -> (b = [u]R -> (x e. b -> (x e. a -> a = b))))
33	32	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- (v e. A -> (a = [v]R -> (b = [u]R -> (x e. b -> (x e. a -> a = b)))))
34	33	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (E.v e. A a = [v]R -> (b = [u]R -> (x e. b -> (x e. a -> a = b))))
35	8, 34	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (a e. (A/.R) -> (b = [u]R -> (x e. b -> (x e. a -> a = b))))
36	35	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (b = [u]R -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
37	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (u e. A -> (b = [u]R -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b)))))
38	37	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (E.u e. A b = [u]R -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
39	6, 38	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (b e. (A/.R) -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
40	4, 39	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((b e. B /\ (b e. B -> b e. (A/.R))) -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
41	40	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (b e. B -> ((b e. B -> b e. (A/.R)) -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b)))))
42	41	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (b e. B -> (x e. b -> ((b e. B -> b e. (A/.R)) -> (a e. (A/.R) -> (x e. a -> a = b)))))
43	42	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((b e. B /\ x e. b) -> ((b e. B -> b e. (A/.R)) -> (a e. (A/.R) -> (x e. a -> a = b))))
44	43	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (a e. (A/.R) -> ((b e. B -> b e. (A/.R)) -> ((b e. B /\ x e. b) -> (x e. a -> a = b))))
45	3, 44	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((a e. C /\ (a e. C -> a e. (A/.R))) -> ((b e. B -> b e. (A/.R)) -> ((b e. B /\ x e. b) -> (x e. a -> a = b))))
46	45	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (a e. C -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> ((b e. B /\ x e. b) -> (x e. a -> a = b)))))
47	46	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (a e. C -> ((b e. B /\ x e. b) -> ((b e. B -> b e. (A/.R)) -> ((a e. C -> a e. (A/.R)) -> (x e. a -> a = b)))))
48	47	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((a e. C /\ (b e. B /\ x e. b)) -> ((b e. B -> b e. (A/.R)) -> ((a e. C -> a e. (A/.R)) -> (x e. a -> a = b))))
49	48	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((a e. C /\ (b e. B /\ x e. b)) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> a = b))))
50	49	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((a e. C /\ (b e. B /\ x e. b)) /\ x e. a) /\ (a e. C -> a e. (A/.R))) -> ((b e. B -> b e. (A/.R)) -> a = b))
51		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (a = b -> (a e. C <-> b e. C))
52		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (b e. (C i^i B) <-> (b e. C /\ b e. B))
53		elequ2 1497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (c = b -> (x e. c <-> x e. b))
54	53	biimprd 171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (c = b -> (x e. b -> x e. c))
55		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (b = c -> (b e. (C i^i B) <-> c e. (C i^i B)))
56		incom 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (C i^i B) = (B i^i C)
57	56	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (c e. (C i^i B) <-> c e. (B i^i C))
58	55, 57	syl6bb 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (b = c -> (b e. (C i^i B) <-> c e. (B i^i C)))
59	58	equcoms 1489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (c = b -> (b e. (C i^i B) <-> c e. (B i^i C)))
60	59	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (c = b -> (b e. (C i^i B) -> c e. (B i^i C)))
61	54, 60	anim12d 617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (c = b -> ((x e. b /\ b e. (C i^i B)) -> (x e. c /\ c e. (B i^i C))))
62	61	a4imev 1650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((x e. b /\ b e. (C i^i B)) -> E.c(x e. c /\ c e. (B i^i C)))
63	62	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (b e. (C i^i B) -> (x e. b -> E.c(x e. c /\ c e. (B i^i C))))
64	52, 63	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((b e. C /\ b e. B) -> (x e. b -> E.c(x e. c /\ c e. (B i^i C))))
65	64	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (b e. C -> (b e. B -> (x e. b -> E.c(x e. c /\ c e. (B i^i C)))))
66	51, 65	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (a = b -> (a e. C -> (b e. B -> (x e. b -> E.c(x e. c /\ c e. (B i^i C))))))
67	66	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (a e. C -> (b e. B -> (a = b -> (x e. b -> E.c(x e. c /\ c e. (B i^i C))))))
68	67	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((a e. C /\ b e. B) -> (a = b -> (x e. b -> E.c(x e. c /\ c e. (B i^i C)))))
69	68	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((a e. C /\ b e. B) -> (x e. b -> (a = b -> E.c(x e. c /\ c e. (B i^i C)))))
70	69	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((a e. C /\ b e. B) /\ x e. b) -> (a = b -> E.c(x e. c /\ c e. (B i^i C))))
71	50, 70	syl9 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((a e. C /\ (b e. B /\ x e. b)) /\ x e. a) /\ (a e. C -> a e. (A/.R))) -> (((a e. C /\ b e. B) /\ x e. b) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))
72	71	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((a e. C /\ (b e. B /\ x e. b)) /\ x e. a) -> ((a e. C -> a e. (A/.R)) -> (((a e. C /\ b e. B) /\ x e. b) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))
73	72	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((a e. C /\ (b e. B /\ x e. b)) /\ x e. a) -> (((a e. C /\ b e. B) /\ x e. b) -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))
74	73	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((a e. C /\ (b e. B /\ x e. b)) -> (x e. a -> (((a e. C /\ b e. B) /\ x e. b) -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))
75	74	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((a e. C /\ (b e. B /\ x e. b)) -> (((a e. C /\ b e. B) /\ x e. b) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))
76	75	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (a e. C -> ((b e. B /\ x e. b) -> (((a e. C /\ b e. B) /\ x e. b) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))))
77	76	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((a e. C /\ b e. B) /\ x e. b) -> (a e. C -> ((b e. B /\ x e. b) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))))
78	77	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((a e. C /\ b e. B) -> (x e. b -> (a e. C -> ((b e. B /\ x e. b) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))))
79	78	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((a e. C /\ b e. B) -> (a e. C -> (x e. b -> ((b e. B /\ x e. b) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))))
80	79	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a e. C -> (b e. B -> (a e. C -> (x e. b -> ((b e. B /\ x e. b) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))))))
81	80	pm2.43a 80	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (a e. C -> (b e. B -> (x e. b -> ((b e. B /\ x e. b) -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))))
82	81	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((b e. B /\ x e. b) -> (b e. B -> (x e. b -> (a e. C -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))))
83	82	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b e. B -> (x e. b -> (b e. B -> (x e. b -> (a e. C -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))))))
84	83	pm2.43a 80	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (b e. B -> (x e. b -> (x e. b -> (a e. C -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))))
85	84	com13 37	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. b -> (x e. b -> (b e. B -> (a e. C -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))))
86	85	pm2.43i 78	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. b -> (b e. B -> (a e. C -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))))
87	86	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. b /\ b e. B) -> (a e. C -> (x e. a -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))
88	87	com13 37	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. a -> (a e. C -> ((x e. b /\ b e. B) -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C)))))))
89	88	imp 377	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> E.c(x e. c /\ c e. (B i^i C))))))
90	89	com4t 44	. . . . . . . . . . . . . . . . . . 19 |- ((a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C))))))
91	90	a4s 1330	. . . . . . . . . . . . . . . . . 18 |- (A.a(a e. C -> a e. (A/.R)) -> ((b e. B -> b e. (A/.R)) -> ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C))))))
92	2, 91	sylbi 216	. . . . . . . . . . . . . . . . 17 |- (C C_ (A/.R) -> ((b e. B -> b e. (A/.R)) -> ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C))))))
93	92	com12 14	. . . . . . . . . . . . . . . 16 |- ((b e. B -> b e. (A/.R)) -> (C C_ (A/.R) -> ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C))))))
94	93	a4s 1330	. . . . . . . . . . . . . . 15 |- (A.b(b e. B -> b e. (A/.R)) -> (C C_ (A/.R) -> ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C))))))
95	1, 94	sylbi 216	. . . . . . . . . . . . . 14 |- (B C_ (A/.R) -> (C C_ (A/.R) -> ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C))))))
96	95	imp 377	. . . . . . . . . . . . 13 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> ((x e. a /\ a e. C) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C)))))
97	96	com12 14	. . . . . . . . . . . 12 |- ((x e. a /\ a e. C) -> ((B C_ (A/.R) /\ C C_ (A/.R)) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C)))))
98	97	19.23aiv 1674	. . . . . . . . . . 11 |- (E.a(x e. a /\ a e. C) -> ((B C_ (A/.R) /\ C C_ (A/.R)) -> ((x e. b /\ b e. B) -> E.c(x e. c /\ c e. (B i^i C)))))
99	98	com13 37	. . . . . . . . . 10 |- ((x e. b /\ b e. B) -> ((B C_ (A/.R) /\ C C_ (A/.R)) -> (E.a(x e. a /\ a e. C) -> E.c(x e. c /\ c e. (B i^i C)))))
100	99	19.23aiv 1674	. . . . . . . . 9 |- (E.b(x e. b /\ b e. B) -> ((B C_ (A/.R) /\ C C_ (A/.R)) -> (E.a(x e. a /\ a e. C) -> E.c(x e. c /\ c e. (B i^i C)))))
101	100	com12 14	. . . . . . . 8 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> (E.b(x e. b /\ b e. B) -> (E.a(x e. a /\ a e. C) -> E.c(x e. c /\ c e. (B i^i C)))))
102		eluni 3180	. . . . . . . 8 |- (x e. U.C <-> E.a(x e. a /\ a e. C))
103	101, 102	syl7ib 233	. . . . . . 7 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> (E.b(x e. b /\ b e. B) -> (x e. U.C -> E.c(x e. c /\ c e. (B i^i C)))))
104		eluni 3180	. . . . . . 7 |- (x e. U.B <-> E.b(x e. b /\ b e. B))
105	103, 104	syl5ib 223	. . . . . 6 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> (x e. U.B -> (x e. U.C -> E.c(x e. c /\ c e. (B i^i C)))))
106	105	imp3a 388	. . . . 5 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> ((x e. U.B /\ x e. U.C) -> E.c(x e. c /\ c e. (B i^i C))))
107		elin 2786	. . . . 5 |- (x e. (U.B i^i U.C) <-> (x e. U.B /\ x e. U.C))
108		eluni 3180	. . . . 5 |- (x e. U.(B i^i C) <-> E.c(x e. c /\ c e. (B i^i C)))
109	106, 107, 108	3imtr4g 612	. . . 4 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> (x e. (U.B i^i U.C) -> x e. U.(B i^i C)))
110	109	ssrdv 2622	. . 3 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> (U.B i^i U.C) C_ U.(B i^i C))
111		uniin 3197	. . 3 |- U.(B i^i C) C_ (U.B i^i U.C)
112	110, 111	jctil 316	. 2 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> (U.(B i^i C) C_ (U.B i^i U.C) /\ (U.B i^i U.C) C_ U.(B i^i C)))
113		eqss 2631	. 2 |- (U.(B i^i C) = (U.B i^i U.C) <-> (U.(B i^i C) C_ (U.B i^i U.C) /\ (U.B i^i U.C) C_ U.(B i^i C)))
114	112, 113	sylibr 217	1 |- ((B C_ (A/.R) /\ C C_ (A/.R)) -> U.(B i^i C) = (U.B i^i U.C))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  E.wrex 2106   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177  Er wer 5315  [cec 5316  /.cqs 5317

This theorem is referenced by:  qusp 14908

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-er 5318  df-ec 5320  df-qs 5323

Copyright terms: Public domain