Theorem disjxun 4437

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 3861	. . . . . . . . . . 11 |- ( ( ( A i^i B ) = (/) /\ x e. A ) -> -. x e. B )
2		eleq1 2526	. . . . . . . . . . . 12 |- ( x = y -> ( x e. B <-> y e. B ) )
3	2	notbid 292	. . . . . . . . . . 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 617	. . . . . . . 8 |- ( ( ( A i^i B ) = (/) /\ ( x e. A /\ y e. B ) ) -> -. x = y )
7		biorf 403	. . . . . . . 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 2896	. . . . 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 701	. . . 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 3671	. . . . . 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 2885	. . . . 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 1712	. . . . . 6 |- F/ z A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) )
15		nfcv 2616	. . . . . . 7 |- F/_ x ( A u. B )
16		nfv 1712	. . . . . . . 8 |- F/ x z = w
17		nfcsb1v 3436	. . . . . . . . . 10 |- F/_ x [_ z / x ]_ C
18		nfcsb1v 3436	. . . . . . . . . 10 |- F/_ x [_ w / x ]_ C
19	17, 18	nfin 3691	. . . . . . . . 9 |- F/_ x ( [_ z / x ]_ C i^i [_ w / x ]_ C )
20	19	nfeq1 2631	. . . . . . . 8 |- F/ x ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/)
21	16, 20	nfor 1940	. . . . . . 7 |- F/ x ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
22	15, 21	nfral 2840	. . . . . 6 |- F/ x A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
23		equequ2 1804	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
24		nfcv 2616	. . . . . . . . . . . 12 |- F/_ x y
25		nfcv 2616	. . . . . . . . . . . 12 |- F/_ x D
26		disjxun.1	. . . . . . . . . . . 12 |- ( x = y -> C = D )
27	24, 25, 26	csbhypf 3439	. . . . . . . . . . 11 |- ( w = y -> [_ w / x ]_ C = D )
28	27	ineq2d 3686	. . . . . . . . . 10 |- ( w = y -> ( C i^i [_ w / x ]_ C ) = ( C i^i D ) )
29	28	eqeq1d 2456	. . . . . . . . 9 |- ( w = y -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( C i^i D ) = (/) ) )
30	23, 29	orbi12d 707	. . . . . . . 8 |- ( w = y -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
31	30	cbvralv 3081	. . . . . . 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 1803	. . . . . . . . 9 |- ( x = z -> ( x = w <-> z = w ) )
33		csbeq1a 3429	. . . . . . . . . . 11 |- ( x = z -> C = [_ z / x ]_ C )
34	33	ineq1d 3685	. . . . . . . . . 10 |- ( x = z -> ( C i^i [_ w / x ]_ C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
35	34	eqeq1d 2456	. . . . . . . . 9 |- ( x = z -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
36	32, 35	orbi12d 707	. . . . . . . 8 |- ( x = z -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
37	36	ralbidv 2893	. . . . . . 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 3077	. . . . 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 2981	. . . . 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 4424	. . . . 5 |- (Disj x e. A C <-> A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) )
43	42	anbi1i 693	. . . 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 1712	. . . . . . . . . 10 |- F/ w ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) )
46		equequ2 1804	. . . . . . . . . . 11 |- ( x = w -> ( z = x <-> z = w ) )
47		csbeq1a 3429	. . . . . . . . . . . . 13 |- ( x = w -> C = [_ w / x ]_ C )
48	47	ineq2d 3686	. . . . . . . . . . . 12 |- ( x = w -> ( [_ z / x ]_ C i^i C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
49	48	eqeq1d 2456	. . . . . . . . . . 11 |- ( x = w -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
50	46, 49	orbi12d 707	. . . . . . . . . 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 3077	. . . . . . . . 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 1803	. . . . . . . . . . . 12 |- ( z = y -> ( z = x <-> y = x ) )
53		equcom 1799	. . . . . . . . . . . 12 |- ( y = x <-> x = y )
54	52, 53	syl6bb 261	. . . . . . . . . . 11 |- ( z = y -> ( z = x <-> x = y ) )
55	24, 25, 26	csbhypf 3439	. . . . . . . . . . . . . 14 |- ( z = y -> [_ z / x ]_ C = D )
56	55	ineq1d 3685	. . . . . . . . . . . . 13 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( D i^i C ) )
57		incom 3677	. . . . . . . . . . . . 13 |- ( D i^i C ) = ( C i^i D )
58	56, 57	syl6eq 2511	. . . . . . . . . . . 12 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( C i^i D ) )
59	58	eqeq1d 2456	. . . . . . . . . . 11 |- ( z = y -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( C i^i D ) = (/) ) )
60	54, 59	orbi12d 707	. . . . . . . . . 10 |- ( z = y -> ( ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
61	60	ralbidv 2893	. . . . . . . . 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 3081	. . . . . . 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 3015	. . . . . . 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 702	. . . 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 3671	. . . . . 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 2885	. . . . 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 2981	. . . . 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 4425	. . . . 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 694	. . . 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 708	. 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 4425	. . 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 3671	. . 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 973	. . 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 827	. . 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 366   /\ wa 367   /\ w3a 971   = wceq 1398   e. wcel 1823   A.wral 2804   [_csb 3420   u. cun 3459   i^i cin 3460   (/)c0 3783  Disj wdisj 4410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-nul 3784  df-disj 4411

This theorem is referenced by: (None)