disjxiun

Description: An indexed union of a disjoint collection of disjoint collections is disjoint if each component is disjoint, and the disjoint unions in the collection are also disjoint. Note that B ( y ) and C ( x ) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016) (Proof shortened by JJ, 27-May-2021)

		Ref	Expression
	Assertion	disjxiun	$⊢ \underset{y \in A}{Disj} B \to (\underset{x \in ⋃_{y \in A} B}{Disj} C \leftrightarrow (\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C))$

Proof

Step	Hyp	Ref	Expression
1		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in A} B$
2		nfcv	$⊢ \underline{Ⅎ} y C$
3	1 2	nfdisjw	$⊢ Ⅎ y \underset{x \in ⋃_{y \in A} B}{Disj} C$
4		disjss1	$⊢ B \subseteq ⋃_{y \in A} B \to (\underset{x \in ⋃_{y \in A} B}{Disj} C \to \underset{x \in B}{Disj} C)$
5		ssiun2	$⊢ y \in A \to B \subseteq ⋃_{y \in A} B$
6	4 5	syl11	$⊢ \underset{x \in ⋃_{y \in A} B}{Disj} C \to (y \in A \to \underset{x \in B}{Disj} C)$
7	3 6	ralrimi	$⊢ \underset{x \in ⋃_{y \in A} B}{Disj} C \to \forall y \in A \underset{x \in B}{Disj} C$
8	7	a1i	$⊢ \underset{y \in A}{Disj} B \to (\underset{x \in ⋃_{y \in A} B}{Disj} C \to \forall y \in A \underset{x \in B}{Disj} C)$
9		simplr	$⊢ ((\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \land ((u \in A \land v \in A) \land \neg u = v)) \to \underset{x \in ⋃_{y \in A} B}{Disj} C$
10		ssiun2	$⊢ u \in A \to ⦋ u / y ⦌ B \subseteq ⋃_{u \in A} ⦋ u / y ⦌ B$
11		nfcv	$⊢ \underline{Ⅎ} u B$
12		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ u / y ⦌ B$
13		csbeq1a	$⊢ y = u \to B = ⦋ u / y ⦌ B$
14	11 12 13	cbviun	$⊢ ⋃_{y \in A} B = ⋃_{u \in A} ⦋ u / y ⦌ B$
15	10 14	sseqtrrdi	$⊢ u \in A \to ⦋ u / y ⦌ B \subseteq ⋃_{y \in A} B$
16	15	adantr	$⊢ (u \in A \land v \in A) \to ⦋ u / y ⦌ B \subseteq ⋃_{y \in A} B$
17	16	ad2antrl	$⊢ ((\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \land ((u \in A \land v \in A) \land \neg u = v)) \to ⦋ u / y ⦌ B \subseteq ⋃_{y \in A} B$
18		csbeq1	$⊢ u = v \to ⦋ u / y ⦌ B = ⦋ v / y ⦌ B$
19	18	sseq1d	$⊢ u = v \to (⦋ u / y ⦌ B \subseteq ⋃_{y \in A} B \leftrightarrow ⦋ v / y ⦌ B \subseteq ⋃_{y \in A} B)$
20	19 15	vtoclga	$⊢ v \in A \to ⦋ v / y ⦌ B \subseteq ⋃_{y \in A} B$
21	20	adantl	$⊢ (u \in A \land v \in A) \to ⦋ v / y ⦌ B \subseteq ⋃_{y \in A} B$
22	21	ad2antrl	$⊢ ((\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \land ((u \in A \land v \in A) \land \neg u = v)) \to ⦋ v / y ⦌ B \subseteq ⋃_{y \in A} B$
23	11 12 13	cbvdisj	$⊢ \underset{y \in A}{Disj} B \leftrightarrow \underset{u \in A}{Disj} ⦋ u / y ⦌ B$
24	18	disjor	$⊢ \underset{u \in A}{Disj} ⦋ u / y ⦌ B \leftrightarrow \forall u \in A \forall v \in A (u = v \lor ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset)$
25	23 24	sylbb	$⊢ \underset{y \in A}{Disj} B \to \forall u \in A \forall v \in A (u = v \lor ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset)$
26		rsp2	$⊢ \forall u \in A \forall v \in A (u = v \lor ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset) \to ((u \in A \land v \in A) \to (u = v \lor ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset))$
27	25 26	syl	$⊢ \underset{y \in A}{Disj} B \to ((u \in A \land v \in A) \to (u = v \lor ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset))$
28	27	imp	$⊢ (\underset{y \in A}{Disj} B \land (u \in A \land v \in A)) \to (u = v \lor ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset)$
29	28	ord	$⊢ (\underset{y \in A}{Disj} B \land (u \in A \land v \in A)) \to (\neg u = v \to ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset)$
30	29	impr	$⊢ (\underset{y \in A}{Disj} B \land ((u \in A \land v \in A) \land \neg u = v)) \to ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset$
31	30	adantlr	$⊢ ((\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \land ((u \in A \land v \in A) \land \neg u = v)) \to ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset$
32		disjiun	$⊢ (\underset{x \in ⋃_{y \in A} B}{Disj} C \land (⦋ u / y ⦌ B \subseteq ⋃_{y \in A} B \land ⦋ v / y ⦌ B \subseteq ⋃_{y \in A} B \land ⦋ u / y ⦌ B \cap ⦋ v / y ⦌ B = \emptyset)) \to ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset$
33	9 17 22 31 32	syl13anc	$⊢ ((\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \land ((u \in A \land v \in A) \land \neg u = v)) \to ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset$
34	33	expr	$⊢ ((\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \land (u \in A \land v \in A)) \to (\neg u = v \to ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset)$
35	34	orrd	$⊢ ((\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \land (u \in A \land v \in A)) \to (u = v \lor ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset)$
36	35	ralrimivva	$⊢ (\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \to \forall u \in A \forall v \in A (u = v \lor ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset)$
37	18	iuneq1d	$⊢ u = v \to ⋃_{x \in ⦋ u / y ⦌ B} C = ⋃_{x \in ⦋ v / y ⦌ B} C$
38	37	disjor	$⊢ \underset{u \in A}{Disj} ⋃_{x \in ⦋ u / y ⦌ B} C \leftrightarrow \forall u \in A \forall v \in A (u = v \lor ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset)$
39	36 38	sylibr	$⊢ (\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \to \underset{u \in A}{Disj} ⋃_{x \in ⦋ u / y ⦌ B} C$
40		nfcv	$⊢ \underline{Ⅎ} u ⋃_{x \in B} C$
41	12 2	nfiun	$⊢ \underline{Ⅎ} y ⋃_{x \in ⦋ u / y ⦌ B} C$
42	13	iuneq1d	$⊢ y = u \to ⋃_{x \in B} C = ⋃_{x \in ⦋ u / y ⦌ B} C$
43	40 41 42	cbvdisj	$⊢ \underset{y \in A}{Disj} ⋃_{x \in B} C \leftrightarrow \underset{u \in A}{Disj} ⋃_{x \in ⦋ u / y ⦌ B} C$
44	39 43	sylibr	$⊢ (\underset{y \in A}{Disj} B \land \underset{x \in ⋃_{y \in A} B}{Disj} C) \to \underset{y \in A}{Disj} ⋃_{x \in B} C$
45	44	ex	$⊢ \underset{y \in A}{Disj} B \to (\underset{x \in ⋃_{y \in A} B}{Disj} C \to \underset{y \in A}{Disj} ⋃_{x \in B} C)$
46	8 45	jcad	$⊢ \underset{y \in A}{Disj} B \to (\underset{x \in ⋃_{y \in A} B}{Disj} C \to (\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C))$
47	14	eleq2i	$⊢ r \in ⋃_{y \in A} B \leftrightarrow r \in ⋃_{u \in A} ⦋ u / y ⦌ B$
48		eliun	$⊢ r \in ⋃_{u \in A} ⦋ u / y ⦌ B \leftrightarrow \exists u \in A r \in ⦋ u / y ⦌ B$
49	47 48	bitri	$⊢ r \in ⋃_{y \in A} B \leftrightarrow \exists u \in A r \in ⦋ u / y ⦌ B$
50		nfcv	$⊢ \underline{Ⅎ} v B$
51		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ v / y ⦌ B$
52		csbeq1a	$⊢ y = v \to B = ⦋ v / y ⦌ B$
53	50 51 52	cbviun	$⊢ ⋃_{y \in A} B = ⋃_{v \in A} ⦋ v / y ⦌ B$
54	53	eleq2i	$⊢ s \in ⋃_{y \in A} B \leftrightarrow s \in ⋃_{v \in A} ⦋ v / y ⦌ B$
55		eliun	$⊢ s \in ⋃_{v \in A} ⦋ v / y ⦌ B \leftrightarrow \exists v \in A s \in ⦋ v / y ⦌ B$
56	54 55	bitri	$⊢ s \in ⋃_{y \in A} B \leftrightarrow \exists v \in A s \in ⦋ v / y ⦌ B$
57	49 56	anbi12i	$⊢ (r \in ⋃_{y \in A} B \land s \in ⋃_{y \in A} B) \leftrightarrow (\exists u \in A r \in ⦋ u / y ⦌ B \land \exists v \in A s \in ⦋ v / y ⦌ B)$
58		reeanv	$⊢ \exists u \in A \exists v \in A (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \leftrightarrow (\exists u \in A r \in ⦋ u / y ⦌ B \land \exists v \in A s \in ⦋ v / y ⦌ B)$
59	57 58	bitr4i	$⊢ (r \in ⋃_{y \in A} B \land s \in ⋃_{y \in A} B) \leftrightarrow \exists u \in A \exists v \in A (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)$
60		simplrr	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \land u = v) \to \neg r = s$
61	12 2	nfdisjw	$⊢ Ⅎ y \underset{x \in ⦋ u / y ⦌ B}{Disj} C$
62	13	disjeq1d	$⊢ y = u \to (\underset{x \in B}{Disj} C \leftrightarrow \underset{x \in ⦋ u / y ⦌ B}{Disj} C)$
63	61 62	rspc	$⊢ u \in A \to (\forall y \in A \underset{x \in B}{Disj} C \to \underset{x \in ⦋ u / y ⦌ B}{Disj} C)$
64	63	impcom	$⊢ (\forall y \in A \underset{x \in B}{Disj} C \land u \in A) \to \underset{x \in ⦋ u / y ⦌ B}{Disj} C$
65		disjors	$⊢ \underset{x \in ⦋ u / y ⦌ B}{Disj} C \leftrightarrow \forall r \in ⦋ u / y ⦌ B \forall s \in ⦋ u / y ⦌ B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
66	64 65	sylib	$⊢ (\forall y \in A \underset{x \in B}{Disj} C \land u \in A) \to \forall r \in ⦋ u / y ⦌ B \forall s \in ⦋ u / y ⦌ B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
67	66	ad2ant2r	$⊢ ((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \to \forall r \in ⦋ u / y ⦌ B \forall s \in ⦋ u / y ⦌ B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
68	67	adantr	$⊢ (((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \to \forall r \in ⦋ u / y ⦌ B \forall s \in ⦋ u / y ⦌ B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
69		simplrl	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \land u = v) \to r \in ⦋ u / y ⦌ B$
70		simplrr	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \land u = v) \to s \in ⦋ v / y ⦌ B$
71	18	adantl	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \land u = v) \to ⦋ u / y ⦌ B = ⦋ v / y ⦌ B$
72	70 71	eleqtrrd	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \land u = v) \to s \in ⦋ u / y ⦌ B$
73	69 72	jca	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \land u = v) \to (r \in ⦋ u / y ⦌ B \land s \in ⦋ u / y ⦌ B)$
74		rsp2	$⊢ \forall r \in ⦋ u / y ⦌ B \forall s \in ⦋ u / y ⦌ B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset) \to ((r \in ⦋ u / y ⦌ B \land s \in ⦋ u / y ⦌ B) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset))$
75	74	imp	$⊢ (\forall r \in ⦋ u / y ⦌ B \forall s \in ⦋ u / y ⦌ B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ u / y ⦌ B)) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
76	68 73 75	syl2an2r	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \land u = v) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
77	76	adantlrr	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \land u = v) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
78	77	ord	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \land u = v) \to (\neg r = s \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
79	60 78	mpd	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \land u = v) \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset$
80		ssiun2	$⊢ r \in ⦋ u / y ⦌ B \to ⦋ r / x ⦌ C \subseteq ⋃_{r \in ⦋ u / y ⦌ B} ⦋ r / x ⦌ C$
81		nfcv	$⊢ \underline{Ⅎ} r C$
82		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ r / x ⦌ C$
83		csbeq1a	$⊢ x = r \to C = ⦋ r / x ⦌ C$
84	81 82 83	cbviun	$⊢ ⋃_{x \in ⦋ u / y ⦌ B} C = ⋃_{r \in ⦋ u / y ⦌ B} ⦋ r / x ⦌ C$
85	80 84	sseqtrrdi	$⊢ r \in ⦋ u / y ⦌ B \to ⦋ r / x ⦌ C \subseteq ⋃_{x \in ⦋ u / y ⦌ B} C$
86		ssiun2	$⊢ s \in ⦋ v / y ⦌ B \to ⦋ s / x ⦌ C \subseteq ⋃_{s \in ⦋ v / y ⦌ B} ⦋ s / x ⦌ C$
87		nfcv	$⊢ \underline{Ⅎ} s C$
88		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ C$
89		csbeq1a	$⊢ x = s \to C = ⦋ s / x ⦌ C$
90	87 88 89	cbviun	$⊢ ⋃_{x \in ⦋ v / y ⦌ B} C = ⋃_{s \in ⦋ v / y ⦌ B} ⦋ s / x ⦌ C$
91	86 90	sseqtrrdi	$⊢ s \in ⦋ v / y ⦌ B \to ⦋ s / x ⦌ C \subseteq ⋃_{x \in ⦋ v / y ⦌ B} C$
92		ss2in	$⊢ (⦋ r / x ⦌ C \subseteq ⋃_{x \in ⦋ u / y ⦌ B} C \land ⦋ s / x ⦌ C \subseteq ⋃_{x \in ⦋ v / y ⦌ B} C) \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C \subseteq ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C$
93	85 91 92	syl2an	$⊢ (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C \subseteq ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C$
94	93	ad2antrl	$⊢ (((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C \subseteq ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C$
95		nfcv	$⊢ \underline{Ⅎ} z ⋃_{x \in B} C$
96		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ z / y ⦌ B$
97	96 2	nfiun	$⊢ \underline{Ⅎ} y ⋃_{x \in ⦋ z / y ⦌ B} C$
98		csbeq1a	$⊢ y = z \to B = ⦋ z / y ⦌ B$
99	98	iuneq1d	$⊢ y = z \to ⋃_{x \in B} C = ⋃_{x \in ⦋ z / y ⦌ B} C$
100	95 97 99	cbvdisj	$⊢ \underset{y \in A}{Disj} ⋃_{x \in B} C \leftrightarrow \underset{z \in A}{Disj} ⋃_{x \in ⦋ z / y ⦌ B} C$
101	100	biimpi	$⊢ \underset{y \in A}{Disj} ⋃_{x \in B} C \to \underset{z \in A}{Disj} ⋃_{x \in ⦋ z / y ⦌ B} C$
102	101	ad3antlr	$⊢ (((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \to \underset{z \in A}{Disj} ⋃_{x \in ⦋ z / y ⦌ B} C$
103		simplr	$⊢ (((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \to (u \in A \land v \in A)$
104		id	$⊢ u \neq v \to u \neq v$
105		csbeq1	$⊢ z = u \to ⦋ z / y ⦌ B = ⦋ u / y ⦌ B$
106	105	iuneq1d	$⊢ z = u \to ⋃_{x \in ⦋ z / y ⦌ B} C = ⋃_{x \in ⦋ u / y ⦌ B} C$
107		csbeq1	$⊢ z = v \to ⦋ z / y ⦌ B = ⦋ v / y ⦌ B$
108	107	iuneq1d	$⊢ z = v \to ⋃_{x \in ⦋ z / y ⦌ B} C = ⋃_{x \in ⦋ v / y ⦌ B} C$
109	106 108	disji2	$⊢ (\underset{z \in A}{Disj} ⋃_{x \in ⦋ z / y ⦌ B} C \land (u \in A \land v \in A) \land u \neq v) \to ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset$
110	102 103 104 109	syl2an3an	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \land u \neq v) \to ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset$
111		sseq0	$⊢ (⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C \subseteq ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C \land ⋃_{x \in ⦋ u / y ⦌ B} C \cap ⋃_{x \in ⦋ v / y ⦌ B} C = \emptyset) \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset$
112	94 110 111	syl2an2r	$⊢ ((((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \land u \neq v) \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset$
113	79 112	pm2.61dane	$⊢ (((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \land \neg r = s)) \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset$
114	113	expr	$⊢ (((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \to (\neg r = s \to ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
115	114	orrd	$⊢ (((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \land (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B)) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
116	115	ex	$⊢ ((\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \land (u \in A \land v \in A)) \to ((r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset))$
117	116	rexlimdvva	$⊢ (\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \to (\exists u \in A \exists v \in A (r \in ⦋ u / y ⦌ B \land s \in ⦋ v / y ⦌ B) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset))$
118	59 117	biimtrid	$⊢ (\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \to ((r \in ⋃_{y \in A} B \land s \in ⋃_{y \in A} B) \to (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset))$
119	118	ralrimivv	$⊢ (\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \to \forall r \in ⋃_{y \in A} B \forall s \in ⋃_{y \in A} B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
120		disjors	$⊢ \underset{x \in ⋃_{y \in A} B}{Disj} C \leftrightarrow \forall r \in ⋃_{y \in A} B \forall s \in ⋃_{y \in A} B (r = s \lor ⦋ r / x ⦌ C \cap ⦋ s / x ⦌ C = \emptyset)$
121	119 120	sylibr	$⊢ (\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C) \to \underset{x \in ⋃_{y \in A} B}{Disj} C$
122	46 121	impbid1	$⊢ \underset{y \in A}{Disj} B \to (\underset{x \in ⋃_{y \in A} B}{Disj} C \leftrightarrow (\forall y \in A \underset{x \in B}{Disj} C \land \underset{y \in A}{Disj} ⋃_{x \in B} C))$

Metamath Proof Explorer

Theorem disjxiun

Proof