Theorem disjxun 4431

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 3855	. . . . . . . . . . 11 |- ( ( ( A i^i B ) = (/) /\ x e. A ) -> -. x e. B )
2		eleq1 2513	. . . . . . . . . . . 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 619	. . . . . . . 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 2883	. . . . 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 703	. . . 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 3667	. . . . . 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 2872	. . . . 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 1692	. . . . . 6 |- F/ z A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) )
15		nfcv 2603	. . . . . . 7 |- F/_ x ( A u. B )
16		nfv 1692	. . . . . . . 8 |- F/ x z = w
17		nfcsb1v 3433	. . . . . . . . . 10 |- F/_ x [_ z / x ]_ C
18		nfcsb1v 3433	. . . . . . . . . 10 |- F/_ x [_ w / x ]_ C
19	17, 18	nfin 3687	. . . . . . . . 9 |- F/_ x ( [_ z / x ]_ C i^i [_ w / x ]_ C )
20	19	nfeq1 2618	. . . . . . . 8 |- F/ x ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/)
21	16, 20	nfor 1919	. . . . . . 7 |- F/ x ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
22	15, 21	nfral 2827	. . . . . 6 |- F/ x A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
23		equequ2 1783	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
24		nfcv 2603	. . . . . . . . . . . 12 |- F/_ x y
25		nfcv 2603	. . . . . . . . . . . 12 |- F/_ x D
26		disjxun.1	. . . . . . . . . . . 12 |- ( x = y -> C = D )
27	24, 25, 26	csbhypf 3436	. . . . . . . . . . 11 |- ( w = y -> [_ w / x ]_ C = D )
28	27	ineq2d 3682	. . . . . . . . . 10 |- ( w = y -> ( C i^i [_ w / x ]_ C ) = ( C i^i D ) )
29	28	eqeq1d 2443	. . . . . . . . 9 |- ( w = y -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( C i^i D ) = (/) ) )
30	23, 29	orbi12d 709	. . . . . . . 8 |- ( w = y -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
31	30	cbvralv 3068	. . . . . . 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 1782	. . . . . . . . 9 |- ( x = z -> ( x = w <-> z = w ) )
33		csbeq1a 3426	. . . . . . . . . . 11 |- ( x = z -> C = [_ z / x ]_ C )
34	33	ineq1d 3681	. . . . . . . . . 10 |- ( x = z -> ( C i^i [_ w / x ]_ C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
35	34	eqeq1d 2443	. . . . . . . . 9 |- ( x = z -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
36	32, 35	orbi12d 709	. . . . . . . 8 |- ( x = z -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
37	36	ralbidv 2880	. . . . . . 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 3064	. . . . 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 2968	. . . . 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 4417	. . . . 5 |- (Disj x e. A C <-> A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) )
43	42	anbi1i 695	. . . 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 1692	. . . . . . . . . 10 |- F/ w ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) )
46		equequ2 1783	. . . . . . . . . . 11 |- ( x = w -> ( z = x <-> z = w ) )
47		csbeq1a 3426	. . . . . . . . . . . . 13 |- ( x = w -> C = [_ w / x ]_ C )
48	47	ineq2d 3682	. . . . . . . . . . . 12 |- ( x = w -> ( [_ z / x ]_ C i^i C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
49	48	eqeq1d 2443	. . . . . . . . . . 11 |- ( x = w -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
50	46, 49	orbi12d 709	. . . . . . . . . 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 3064	. . . . . . . . 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 1782	. . . . . . . . . . . 12 |- ( z = y -> ( z = x <-> y = x ) )
53		equcom 1778	. . . . . . . . . . . 12 |- ( y = x <-> x = y )
54	52, 53	syl6bb 261	. . . . . . . . . . 11 |- ( z = y -> ( z = x <-> x = y ) )
55	24, 25, 26	csbhypf 3436	. . . . . . . . . . . . . 14 |- ( z = y -> [_ z / x ]_ C = D )
56	55	ineq1d 3681	. . . . . . . . . . . . 13 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( D i^i C ) )
57		incom 3673	. . . . . . . . . . . . 13 |- ( D i^i C ) = ( C i^i D )
58	56, 57	syl6eq 2498	. . . . . . . . . . . 12 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( C i^i D ) )
59	58	eqeq1d 2443	. . . . . . . . . . 11 |- ( z = y -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( C i^i D ) = (/) ) )
60	54, 59	orbi12d 709	. . . . . . . . . 10 |- ( z = y -> ( ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
61	60	ralbidv 2880	. . . . . . . . 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 3068	. . . . . . 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 3002	. . . . . . 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 704	. . . 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 3667	. . . . . 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 2872	. . . . 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 2968	. . . . 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 4419	. . . . 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 696	. . . 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 710	. 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 4419	. . 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 3667	. . 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 974	. . 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 368   /\ wa 369   /\ w3a 972   = wceq 1381   e. wcel 1802   A.wral 2791   [_csb 3417   u. cun 3456   i^i cin 3457   (/)c0 3767  Disj wdisj 4403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-nul 3768  df-disj 4404

This theorem is referenced by: (None)