Theorem uninqs 10378

Description: The class union of the intersection of two subclasses of a quotient space. Compare uniin 2515.

Hypothesis

Ref	Expression
uninqs.1	|- Er R

Assertion

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

Proof of Theorem uninqs

Step	Hyp	Ref	Expression
1		dfss2 2054	. . . . . . . . . . . . . . 15 |- (B (_ (A/.R) <-> A.b(b e. B -> b e. (A/.R)))
2		dfss2 2054	. . . . . . . . . . . . . . . . . 18 |- (C (_ (A/.R) <-> A.a(a e. C -> a e. (A/.R)))
3		pm3.35 359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((a e. C /\ (a e. C -> a e. (A/.R))) -> a e. (A/.R))
4		pm3.35 359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((b e. B /\ (b e. B -> b e. (A/.R))) -> b e. (A/.R))
5		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- b e. V
6	5	elqs 4280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (b e. (A/.R) <-> E.u(u e. A /\ b = [u]R))
7		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- a e. V
8	7	elqs 4280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (a e. (A/.R) <-> E.v(v e. A /\ a = [v]R))
9		inelcm 2319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- ((x e. [v]R /\ x e. [u]R) -> ([v]R i^i [u]R) =/= (/))
10		df-ne 1584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 |- (([v]R i^i [u]R) =/= (/) <-> -. ([v]R i^i [u]R) = (/))
11		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- v e. V
12		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- u e. V
13		uninqs.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- Er R
14	11, 12, 13	erdisj 4276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 |- ([v]R = [u]R \/ ([v]R i^i [u]R) = (/))
15		pm5.61 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 |- ((a = [v]R /\ b = [u]R) -> (a = b <-> [v]R = [u]R))
17	16	biimprcd 156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 |- ([v]R = [u]R -> ((a = [v]R /\ b = [u]R) -> a = b))
18	17	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 |- (([v]R = [u]R /\ -. ([v]R i^i [u]R) = (/)) -> ((a = [v]R /\ b = [u]R) -> a = b))
19	15, 18	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 |- (-. ([v]R i^i [u]R) = (/) -> ((a = [v]R /\ b = [u]R) -> a = b))
21	10, 20	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- (([v]R i^i [u]R) =/= (/) -> ((a = [v]R /\ b = [u]R) -> a = b))
22	9, 21	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 |- ((x e. [v]R /\ x e. [u]R) -> ((a = [v]R /\ b = [u]R) -> a = b))
23		eleq2 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- (a = [v]R -> (x e. a <-> x e. [v]R))
24	23	biimpa 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 |- ((a = [v]R /\ x e. a) -> x e. [v]R)
25		eleq2 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 |- (b = [u]R -> (x e. b <-> x e. [u]R))
26	25	biimpa 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 |- ((b = [u]R /\ x e. b) -> x e. [u]R)
27	22, 24, 26	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 |- (((a = [v]R /\ x e. a) /\ (b = [u]R /\ x e. b)) -> ((a = [v]R /\ b = [u]R) -> a = b))
28	27	an4s 508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 |- (((a = [v]R /\ b = [u]R) /\ (x e. a /\ x e. b)) -> ((a = [v]R /\ b = [u]R) -> a = b))
29	28	exp32 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 |- ((a = [v]R /\ b = [u]R) -> (x e. a -> (x e. b -> ((a = [v]R /\ b = [u]R) -> a = b))))
30	29	com24 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 64	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 |- ((a = [v]R /\ b = [u]R) -> (x e. b -> (x e. a -> a = b)))
32	31	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 |- (a = [v]R -> (b = [u]R -> (x e. b -> (x e. a -> a = b))))
33	32	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- ((v e. A /\ a = [v]R) -> (b = [u]R -> (x e. b -> (x e. a -> a = b))))
34	33	19.23aiv 1293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (E.v(v e. A /\ a = [v]R) -> (b = [u]R -> (x e. b -> (x e. a -> a = b))))
35	8, 34	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (a e. (A/.R) -> (b = [u]R -> (x e. b -> (x e. a -> a = b))))
36	35	com3l 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (b = [u]R -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
37	36	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((u e. A /\ b = [u]R) -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
38	37	19.23aiv 1293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (E.u(u e. A /\ b = [u]R) -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
39	6, 38	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (b e. (A/.R) -> (x e. b -> (a e. (A/.R) -> (x e. a -> a = b))))
40	4, 39	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (a = b -> (a e. C <-> b e. C))
52		elin 2203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (b e. (C i^i B) <-> (b e. C /\ b e. B))
53		elequ2 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .