Theorem disjxun 4287

Description: The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.)

Hypothesis

Ref	Expression
disjxun.1	|- ( x = y -> C = D )

Assertion

Ref	Expression
disjxun	|- ( ( A i^i B ) = (/) -> (Disj x e. ( A u. B ) C <-> (Disj x e. A C /\ Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )

Distinct variable groups:   x, y, A   x, B, y   y, C   x, D

Allowed substitution hints:   C( x)   D( y)

Proof of Theorem disjxun

Dummy variables w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		disjel 3722	. . . . . . . . . . 11 |- ( ( ( A i^i B ) = (/) /\ x e. A ) -> -. x e. B )
2		eleq1 2501	. . . . . . . . . . . 12 |- ( x = y -> ( x e. B <-> y e. B ) )
3	2	notbid 294	. . . . . . . . . . 11 |- ( x = y -> ( -. x e. B <-> -. y e. B ) )
4	1, 3	syl5ibcom 220	. . . . . . . . . 10 |- ( ( ( A i^i B ) = (/) /\ x e. A ) -> ( x = y -> -. y e. B ) )
5	4	con2d 115	. . . . . . . . 9 |- ( ( ( A i^i B ) = (/) /\ x e. A ) -> ( y e. B -> -. x = y ) )
6	5	impr 616	. . . . . . . 8 |- ( ( ( A i^i B ) = (/) /\ ( x e. A /\ y e. B ) ) -> -. x = y )
7		biorf 405	. . . . . . . 8 |- ( -. x = y -> ( ( C i^i D ) = (/) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
8	6, 7	syl 16	. . . . . . 7 |- ( ( ( A i^i B ) = (/) /\ ( x e. A /\ y e. B ) ) -> ( ( C i^i D ) = (/) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
9	8	bicomd 201	. . . . . 6 |- ( ( ( A i^i B ) = (/) /\ ( x e. A /\ y e. B ) ) -> ( ( x = y \/ ( C i^i D ) = (/) ) <-> ( C i^i D ) = (/) ) )
10	9	2ralbidva 2753	. . . . 5 |- ( ( A i^i B ) = (/) -> ( A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) <-> A. x e. A A. y e. B ( C i^i D ) = (/) ) )
11	10	anbi2d 698	. . . 4 |- ( ( A i^i B ) = (/) -> ( ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
12		ralunb 3534	. . . . . 6 |- ( A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> ( A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
13	12	ralbii 2737	. . . . 5 |- ( A. x e. A A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> A. x e. A ( A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
14		nfv 1678	. . . . . 6 |- F/ z A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) )
15		nfcv 2577	. . . . . . 7 |- F/_ x ( A u. B )
16		nfv 1678	. . . . . . . 8 |- F/ x z = w
17		nfcsb1v 3301	. . . . . . . . . 10 |- F/_ x [_ z / x ]_ C
18		nfcsb1v 3301	. . . . . . . . . 10 |- F/_ x [_ w / x ]_ C
19	17, 18	nfin 3554	. . . . . . . . 9 |- F/_ x ( [_ z / x ]_ C i^i [_ w / x ]_ C )
20	19	nfeq1 2586	. . . . . . . 8 |- F/ x ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/)
21	16, 20	nfor 1872	. . . . . . 7 |- F/ x ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
22	15, 21	nfral 2767	. . . . . 6 |- F/ x A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
23		equequ2 1742	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
24		nfcv 2577	. . . . . . . . . . . 12 |- F/_ x y
25		nfcv 2577	. . . . . . . . . . . 12 |- F/_ x D
26		disjxun.1	. . . . . . . . . . . 12 |- ( x = y -> C = D )
27	24, 25, 26	csbhypf 3304	. . . . . . . . . . 11 |- ( w = y -> [_ w / x ]_ C = D )
28	27	ineq2d 3549	. . . . . . . . . 10 |- ( w = y -> ( C i^i [_ w / x ]_ C ) = ( C i^i D ) )
29	28	eqeq1d 2449	. . . . . . . . 9 |- ( w = y -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( C i^i D ) = (/) ) )
30	23, 29	orbi12d 704	. . . . . . . 8 |- ( w = y -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
31	30	cbvralv 2945	. . . . . . 7 |- ( A. w e. ( A u. B ) ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) )
32		equequ1 1741	. . . . . . . . 9 |- ( x = z -> ( x = w <-> z = w ) )
33		csbeq1a 3294	. . . . . . . . . . 11 |- ( x = z -> C = [_ z / x ]_ C )
34	33	ineq1d 3548	. . . . . . . . . 10 |- ( x = z -> ( C i^i [_ w / x ]_ C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
35	34	eqeq1d 2449	. . . . . . . . 9 |- ( x = z -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
36	32, 35	orbi12d 704	. . . . . . . 8 |- ( x = z -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
37	36	ralbidv 2733	. . . . . . 7 |- ( x = z -> ( A. w e. ( A u. B ) ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
38	31, 37	syl5bbr 259	. . . . . 6 |- ( x = z -> ( A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
39	14, 22, 38	cbvral 2941	. . . . 5 |- ( A. x e. A A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
40		r19.26 2847	. . . . 5 |- ( A. x e. A ( A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
41	13, 39, 40	3bitr3i 275	. . . 4 |- ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
42	26	disjor 4273	. . . . 5 |- (Disj x e. A C <-> A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) )
43	42	anbi1i 690	. . . 4 |- ( (Disj x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) )
44	11, 41, 43	3bitr4g 288	. . 3 |- ( ( A i^i B ) = (/) -> ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> (Disj x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
45		nfv 1678	. . . . . . . . . 10 |- F/ w ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) )
46		equequ2 1742	. . . . . . . . . . 11 |- ( x = w -> ( z = x <-> z = w ) )
47		csbeq1a 3294	. . . . . . . . . . . . 13 |- ( x = w -> C = [_ w / x ]_ C )
48	47	ineq2d 3549	. . . . . . . . . . . 12 |- ( x = w -> ( [_ z / x ]_ C i^i C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
49	48	eqeq1d 2449	. . . . . . . . . . 11 |- ( x = w -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
50	46, 49	orbi12d 704	. . . . . . . . . 10 |- ( x = w -> ( ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
51	45, 21, 50	cbvral 2941	. . . . . . . . 9 |- ( A. x e. A ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
52		equequ1 1741	. . . . . . . . . . . 12 |- ( z = y -> ( z = x <-> y = x ) )
53		equcom 1737	. . . . . . . . . . . 12 |- ( y = x <-> x = y )
54	52, 53	syl6bb 261	. . . . . . . . . . 11 |- ( z = y -> ( z = x <-> x = y ) )
55	24, 25, 26	csbhypf 3304	. . . . . . . . . . . . . 14 |- ( z = y -> [_ z / x ]_ C = D )
56	55	ineq1d 3548	. . . . . . . . . . . . 13 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( D i^i C ) )
57		incom 3540	. . . . . . . . . . . . 13 |- ( D i^i C ) = ( C i^i D )
58	56, 57	syl6eq 2489	. . . . . . . . . . . 12 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( C i^i D ) )
59	58	eqeq1d 2449	. . . . . . . . . . 11 |- ( z = y -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( C i^i D ) = (/) ) )
60	54, 59	orbi12d 704	. . . . . . . . . 10 |- ( z = y -> ( ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
61	60	ralbidv 2733	. . . . . . . . 9 |- ( z = y -> ( A. x e. A ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> A. x e. A ( x = y \/ ( C i^i D ) = (/) ) ) )
62	51, 61	syl5bbr 259	. . . . . . . 8 |- ( z = y -> ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. x e. A ( x = y \/ ( C i^i D ) = (/) ) ) )
63	62	cbvralv 2945	. . . . . . 7 |- ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. y e. B A. x e. A ( x = y \/ ( C i^i D ) = (/) ) )
64		ralcom 2879	. . . . . . 7 |- ( A. y e. B A. x e. A ( x = y \/ ( C i^i D ) = (/) ) <-> A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) )
65	63, 64	bitri 249	. . . . . 6 |- ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) )
66	65, 10	syl5bb 257	. . . . 5 |- ( ( A i^i B ) = (/) -> ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. x e. A A. y e. B ( C i^i D ) = (/) ) )
67	66	anbi1d 699	. . . 4 |- ( ( A i^i B ) = (/) -> ( ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) <-> ( A. x e. A A. y e. B ( C i^i D ) = (/) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) ) )
68		ralunb 3534	. . . . . 6 |- ( A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
69	68	ralbii 2737	. . . . 5 |- ( A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. z e. B ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
70		r19.26 2847	. . . . 5 |- ( A. z e. B ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) <-> ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
71	69, 70	bitri 249	. . . 4 |- ( A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
72		disjors 4275	. . . . 5 |- (Disj x e. B C <-> A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
73	72	anbi2ci 691	. . . 4 |- ( (Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( A. x e. A A. y e. B ( C i^i D ) = (/) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
74	67, 71, 73	3bitr4g 288	. . 3 |- ( ( A i^i B ) = (/) -> ( A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> (Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
75	44, 74	anbi12d 705	. 2 |- ( ( A i^i B ) = (/) -> ( ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) <-> ( (Disj x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) /\ (Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) ) )
76		disjors 4275	. . 3 |- (Disj x e. ( A u. B ) C <-> A. z e. ( A u. B ) A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
77		ralunb 3534	. . 3 |- ( A. z e. ( A u. B ) A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
78	76, 77	bitri 249	. 2 |- (Disj x e. ( A u. B ) C <-> ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
79		df-3an 962	. . 3 |- ( (Disj x e. A C /\ Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( (Disj x e. A C /\ Disj x e. B C ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) )
80		anandir 820	. . 3 |- ( ( (Disj x e. A C /\ Disj x e. B C ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( (Disj x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) /\ (Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
81	79, 80	bitri 249	. 2 |- ( (Disj x e. A C /\ Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( (Disj x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) /\ (Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
82	75, 78, 81	3bitr4g 288	1 |- ( ( A i^i B ) = (/) -> (Disj x e. ( A u. B ) C <-> (Disj x e. A C /\ Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 960   = wceq 1364   e. wcel 1761   A.wral 2713   [_csb 3285   u. cun 3323   i^i cin 3324   (/)c0 3634  Disj wdisj 4259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-nul 3635  df-disj 4260

This theorem is referenced by: (None)