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	12 2	nfdisjw	$⊢ Ⅎ y \underset{x \in ⦋ u / y ⦌ B}{Disj} C$
61	13	disjeq1d	$⊢ y = u \to (\underset{x \in B}{Disj} C \leftrightarrow \underset{x \in ⦋ u / y ⦌ B}{Disj} C)$
62	60 61	rspc	$⊢ u \in A \to (\forall y \in A \underset{x \in B}{Disj} C \to \underset{x \in ⦋ u / y ⦌ B}{Disj} C)$
63	62	impcom	$⊢ (\forall y \in A \underset{x \in B}{Disj} C \land u \in A) \to \underset{x \in ⦋ u / y ⦌ B}{Disj} C$
64		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)$
65	63 64	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)$
66	65	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)$
67	66	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)$
68		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$
69		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$
70	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$
71	69 70	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$
72	68 71	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)$
73		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))$
74	73	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)$
75	67 72 74	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)$
76	75	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)$
77		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$
78	76 77	orcnd	$⊢ ((((\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$
79		ssiun2	$⊢ r \in ⦋ u / y ⦌ B \to ⦋ r / x ⦌ C \subseteq ⋃_{r \in ⦋ u / y ⦌ B} ⦋ r / x ⦌ C$
80		nfcv	$⊢ \underline{Ⅎ} r C$
81		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ r / x ⦌ C$
82		csbeq1a	$⊢ x = r \to C = ⦋ r / x ⦌ C$
83	80 81 82	cbviun	$⊢ ⋃_{x \in ⦋ u / y ⦌ B} C = ⋃_{r \in ⦋ u / y ⦌ B} ⦋ r / x ⦌ C$
84	79 83	sseqtrrdi	$⊢ r \in ⦋ u / y ⦌ B \to ⦋ r / x ⦌ C \subseteq ⋃_{x \in ⦋ u / y ⦌ B} C$
85		ssiun2	$⊢ s \in ⦋ v / y ⦌ B \to ⦋ s / x ⦌ C \subseteq ⋃_{s \in ⦋ v / y ⦌ B} ⦋ s / x ⦌ C$
86		nfcv	$⊢ \underline{Ⅎ} s C$
87		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ C$
88		csbeq1a	$⊢ x = s \to C = ⦋ s / x ⦌ C$
89	86 87 88	cbviun	$⊢ ⋃_{x \in ⦋ v / y ⦌ B} C = ⋃_{s \in ⦋ v / y ⦌ B} ⦋ s / x ⦌ C$
90	85 89	sseqtrrdi	$⊢ s \in ⦋ v / y ⦌ B \to ⦋ s / x ⦌ C \subseteq ⋃_{x \in ⦋ v / y ⦌ B} C$
91		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$
92	84 90 91	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$
93	92	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$
94		nfcv	$⊢ \underline{Ⅎ} z ⋃_{x \in B} C$
95		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ z / y ⦌ B$
96	95 2	nfiun	$⊢ \underline{Ⅎ} y ⋃_{x \in ⦋ z / y ⦌ B} C$
97		csbeq1a	$⊢ y = z \to B = ⦋ z / y ⦌ B$
98	97	iuneq1d	$⊢ y = z \to ⋃_{x \in B} C = ⋃_{x \in ⦋ z / y ⦌ B} C$
99	94 96 98	cbvdisj	$⊢ \underset{y \in A}{Disj} ⋃_{x \in B} C \leftrightarrow \underset{z \in A}{Disj} ⋃_{x \in ⦋ z / y ⦌ B} C$
100	99	biimpi	$⊢ \underset{y \in A}{Disj} ⋃_{x \in B} C \to \underset{z \in A}{Disj} ⋃_{x \in ⦋ z / y ⦌ B} C$
101	100	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$
102		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)$
103		id	$⊢ u \neq v \to u \neq v$
104		csbeq1	$⊢ z = u \to ⦋ z / y ⦌ B = ⦋ u / y ⦌ B$
105	104	iuneq1d	$⊢ z = u \to ⋃_{x \in ⦋ z / y ⦌ B} C = ⋃_{x \in ⦋ u / y ⦌ B} C$
106		csbeq1	$⊢ z = v \to ⦋ z / y ⦌ B = ⦋ v / y ⦌ B$
107	106	iuneq1d	$⊢ z = v \to ⋃_{x \in ⦋ z / y ⦌ B} C = ⋃_{x \in ⦋ v / y ⦌ B} C$
108	105 107	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$
109	101 102 103 108	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$
110		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$
111	93 109 110	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$
112	78 111	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$
113	112	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)$
114	113	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)$
115	114	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))$
116	115	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))$
117	59 116	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))$
118	117	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)$
119		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)$
120	118 119	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$
121	46 120	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