Theorem erdisj3 16266

Description: Members of a quotient set do not overlap.

Assertion

Ref	Expression
erdisj3	|- (Er R -> ((B e. (A/.R) /\ C e. (A/.R)) -> (B = C \/ (B i^i C) = (/))))

Proof of Theorem erdisj3

Step	Hyp	Ref	Expression
1		eqeq1 1890	. . . . . . . . . . . 12 |- ([x]R = B -> ([x]R = [y]R <-> B = [y]R))
2		ineq1 2789	. . . . . . . . . . . . 13 |- ([x]R = B -> ([x]R i^i [y]R) = (B i^i [y]R))
3	2	eqeq1d 1892	. . . . . . . . . . . 12 |- ([x]R = B -> (([x]R i^i [y]R) = (/) <-> (B i^i [y]R) = (/)))
4	1, 3	orbi12d 689	. . . . . . . . . . 11 |- ([x]R = B -> (([x]R = [y]R \/ ([x]R i^i [y]R) = (/)) <-> (B = [y]R \/ (B i^i [y]R) = (/))))
5		eqeq2 1893	. . . . . . . . . . . 12 |- ([y]R = C -> (B = [y]R <-> B = C))
6		ineq2 2790	. . . . . . . . . . . . 13 |- ([y]R = C -> (B i^i [y]R) = (B i^i C))
7	6	eqeq1d 1892	. . . . . . . . . . . 12 |- ([y]R = C -> ((B i^i [y]R) = (/) <-> (B i^i C) = (/)))
8	5, 7	orbi12d 689	. . . . . . . . . . 11 |- ([y]R = C -> ((B = [y]R \/ (B i^i [y]R) = (/)) <-> (B = C \/ (B i^i C) = (/))))
9	4, 8	sylan9bb 599	. . . . . . . . . 10 |- (([x]R = B /\ [y]R = C) -> (([x]R = [y]R \/ ([x]R i^i [y]R) = (/)) <-> (B = C \/ (B i^i C) = (/))))
10		visset 2295	. . . . . . . . . . 11 |- x e. _V
11		visset 2295	. . . . . . . . . . 11 |- y e. _V
12	10, 11	erdisj2 10164	. . . . . . . . . 10 |- (Er R -> ([x]R = [y]R \/ ([x]R i^i [y]R) = (/)))
13	9, 12	syl5cbi 226	. . . . . . . . 9 |- (Er R -> (([x]R = B /\ [y]R = C) -> (B = C \/ (B i^i C) = (/))))
14	13	exp3a 405	. . . . . . . 8 |- (Er R -> ([x]R = B -> ([y]R = C -> (B = C \/ (B i^i C) = (/)))))
15	14	19.23adv 1584	. . . . . . 7 |- (Er R -> (E.x[x]R = B -> ([y]R = C -> (B = C \/ (B i^i C) = (/)))))
16	15	imp 377	. . . . . 6 |- ((Er R /\ E.x[x]R = B) -> ([y]R = C -> (B = C \/ (B i^i C) = (/))))
17	16	19.23adv 1584	. . . . 5 |- ((Er R /\ E.x[x]R = B) -> (E.y[y]R = C -> (B = C \/ (B i^i C) = (/))))
18	17	ex 402	. . . 4 |- (Er R -> (E.x[x]R = B -> (E.y[y]R = C -> (B = C \/ (B i^i C) = (/)))))
19		elqsi 5349	. . . . . . 7 |- (B e. (A/.R) -> E.x e. A B = [x]R)
20		df-rex 2110	. . . . . . 7 |- (E.x e. A B = [x]R <-> E.x(x e. A /\ B = [x]R))
21	19, 20	sylib 215	. . . . . 6 |- (B e. (A/.R) -> E.x(x e. A /\ B = [x]R))
22		exan3 16241	. . . . . 6 |- (E.x(x e. A /\ B = [x]R) -> E.x B = [x]R)
23	21, 22	syl 12	. . . . 5 |- (B e. (A/.R) -> E.x B = [x]R)
24		eqcom 1886	. . . . . 6 |- (B = [x]R <-> [x]R = B)
25	24	exbii 1398	. . . . 5 |- (E.x B = [x]R <-> E.x[x]R = B)
26	23, 25	sylib 215	. . . 4 |- (B e. (A/.R) -> E.x[x]R = B)
27	18, 26	syl5 20	. . 3 |- (Er R -> (B e. (A/.R) -> (E.y[y]R = C -> (B = C \/ (B i^i C) = (/)))))
28		elqsi 5349	. . . . . 6 |- (C e. (A/.R) -> E.y e. A C = [y]R)
29		df-rex 2110	. . . . . 6 |- (E.y e. A C = [y]R <-> E.y(y e. A /\ C = [y]R))
30	28, 29	sylib 215	. . . . 5 |- (C e. (A/.R) -> E.y(y e. A /\ C = [y]R))
31		exan3 16241	. . . . 5 |- (E.y(y e. A /\ C = [y]R) -> E.y C = [y]R)
32	30, 31	syl 12	. . . 4 |- (C e. (A/.R) -> E.y C = [y]R)
33		eqcom 1886	. . . . 5 |- (C = [y]R <-> [y]R = C)
34	33	exbii 1398	. . . 4 |- (E.y C = [y]R <-> E.y[y]R = C)
35	32, 34	sylib 215	. . 3 |- (C e. (A/.R) -> E.y[y]R = C)
36	27, 35	syl7 26	. 2 |- (Er R -> (B e. (A/.R) -> (C e. (A/.R) -> (B = C \/ (B i^i C) = (/)))))
37	36	imp3a 388	1 |- (Er R -> ((B e. (A/.R) /\ C e. (A/.R)) -> (B = C \/ (B i^i C) = (/))))

Syntax hints:   -> wi 3   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  E.wrex 2106   i^i cin 2592  (/)c0 2875  Er wer 5315  [cec 5316  /.cqs 5317

This theorem is referenced by:  erprt 16276

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-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-id 3586  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