Theorem disjxun 4440

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 3868	. . . . . . . . . . 11 |- ( ( ( A i^i B ) = (/) /\ x e. A ) -> -. x e. B )
2		eleq1 2534	. . . . . . . . . . . 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 2901	. . . . 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 3680	. . . . . 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 2890	. . . . 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 2624	. . . . . . 7 |- F/_ x ( A u. B )
16		nfv 1678	. . . . . . . 8 |- F/ x z = w
17		nfcsb1v 3446	. . . . . . . . . 10 |- F/_ x [_ z / x ]_ C
18		nfcsb1v 3446	. . . . . . . . . 10 |- F/_ x [_ w / x ]_ C
19	17, 18	nfin 3700	. . . . . . . . 9 |- F/_ x ( [_ z / x ]_ C i^i [_ w / x ]_ C )
20	19	nfeq1 2639	. . . . . . . 8 |- F/ x ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/)
21	16, 20	nfor 1877	. . . . . . 7 |- F/ x ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
22	15, 21	nfral 2845	. . . . . 6 |- F/ x A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
23		equequ2 1743	. . . . . . . . 9 |- ( w = y -> ( x = w <-> x = y ) )
24		nfcv 2624	. . . . . . . . . . . 12 |- F/_ x y
25		nfcv 2624	. . . . . . . . . . . 12 |- F/_ x D
26		disjxun.1	. . . . . . . . . . . 12 |- ( x = y -> C = D )
27	24, 25, 26	csbhypf 3449	. . . . . . . . . . 11 |- ( w = y -> [_ w / x ]_ C = D )
28	27	ineq2d 3695	. . . . . . . . . 10 |- ( w = y -> ( C i^i [_ w / x ]_ C ) = ( C i^i D ) )
29	28	eqeq1d 2464	. . . . . . . . 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 3083	. . . . . . 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 1742	. . . . . . . . 9 |- ( x = z -> ( x = w <-> z = w ) )
33		csbeq1a 3439	. . . . . . . . . . 11 |- ( x = z -> C = [_ z / x ]_ C )
34	33	ineq1d 3694	. . . . . . . . . 10 |- ( x = z -> ( C i^i [_ w / x ]_ C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
35	34	eqeq1d 2464	. . . . . . . . 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 2898	. . . . . . 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 3079	. . . . 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 2984	. . . . 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 4426	. . . . 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 1678	. . . . . . . . . 10 |- F/ w ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) )
46		equequ2 1743	. . . . . . . . . . 11 |- ( x = w -> ( z = x <-> z = w ) )
47		csbeq1a 3439	. . . . . . . . . . . . 13 |- ( x = w -> C = [_ w / x ]_ C )
48	47	ineq2d 3695	. . . . . . . . . . . 12 |- ( x = w -> ( [_ z / x ]_ C i^i C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
49	48	eqeq1d 2464	. . . . . . . . . . 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 3079	. . . . . . . . 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 1742	. . . . . . . . . . . 12 |- ( z = y -> ( z = x <-> y = x ) )
53		equcom 1738	. . . . . . . . . . . 12 |- ( y = x <-> x = y )
54	52, 53	syl6bb 261	. . . . . . . . . . 11 |- ( z = y -> ( z = x <-> x = y ) )
55	24, 25, 26	csbhypf 3449	. . . . . . . . . . . . . 14 |- ( z = y -> [_ z / x ]_ C = D )
56	55	ineq1d 3694	. . . . . . . . . . . . 13 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( D i^i C ) )
57		incom 3686	. . . . . . . . . . . . 13 |- ( D i^i C ) = ( C i^i D )
58	56, 57	syl6eq 2519	. . . . . . . . . . . 12 |- ( z = y -> ( [_ z / x ]_ C i^i C ) = ( C i^i D ) )
59	58	eqeq1d 2464	. . . . . . . . . . 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 2898	. . . . . . . . 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 3083	. . . . . . 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 3017	. . . . . . 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 3680	. . . . . 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 2890	. . . . 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 2984	. . . . 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 4428	. . . . 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 4428	. . 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 3680	. . 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 970	. . 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 826	. . 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 968   = wceq 1374   e. wcel 1762   A.wral 2809   [_csb 3430   u. cun 3469   i^i cin 3470   (/)c0 3780  Disj wdisj 4412

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 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-reu 2816  df-rmo 2817  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-nul 3781  df-disj 4413

This theorem is referenced by: (None)