Theorem disjxiun 5146

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 𝐵(𝑦) and 𝐶(𝑥) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by JJ, 27-May-2021.)

Assertion

Ref	Expression
disjxiun	⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵   𝑦,𝐶

Allowed substitution hints:   𝐵(𝑦)   𝐶(𝑥)

Proof of Theorem disjxiun

Dummy variables 𝑠 𝑟 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfiu1 5032	. . . . . 6 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝐴 𝐵
2		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑦𝐶
3	1, 2	nfdisjw 5126	. . . . 5 ⊢ Ⅎ𝑦Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶
4		disjss1 5120	. . . . . 6 ⊢ (𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶))
5		ssiun2 5051	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
6	4, 5	syl11 33	. . . . 5 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (𝑦 ∈ 𝐴 → Disj 𝑥 ∈ 𝐵 𝐶))
7	3, 6	ralrimi 3255	. . . 4 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶)
8	7	a1i 11	. . 3 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶))
9		simplr 768	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶)
10		ssiun2 5051	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
11		nfcv 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑢𝐵
12		nfcsb1v 3919	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑢 / 𝑦⦌𝐵
13		csbeq1a 3908	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑦⦌𝐵)
14	11, 12, 13	cbviun 5040	. . . . . . . . . . . . 13 ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵
15	10, 14	sseqtrrdi 4034	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
16	15	adantr 482	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
17	16	ad2antrl 727	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
18		csbeq1 3897	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑣 → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
19	18	sseq1d 4014	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵))
20	19, 15	vtoclga 3566	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
21	20	adantl 483	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
22	21	ad2antrl 727	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
23	11, 12, 13	cbvdisj 5124	. . . . . . . . . . . . . . . 16 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
24	18	disjor 5129	. . . . . . . . . . . . . . . 16 ⊢ (Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
25	23, 24	sylbb 218	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
26		rsp2 3275	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)))
27	25, 26	syl 17	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)))
28	27	imp 408	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
29	28	ord 863	. . . . . . . . . . . 12 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
30	29	impr 456	. . . . . . . . . . 11 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)
31	30	adantlr 714	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)
32		disjiun 5136	. . . . . . . . . 10 ⊢ ((Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ∧ (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
33	9, 17, 22, 31, 32	syl13anc 1373	. . . . . . . . 9 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
34	33	expr 458	. . . . . . . 8 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
35	34	orrd 862	. . . . . . 7 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
36	35	ralrimivva 3201	. . . . . 6 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
37	18	iuneq1d 5025	. . . . . . 7 ⊢ (𝑢 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
38	37	disjor 5129	. . . . . 6 ⊢ (Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
39	36, 38	sylibr 233	. . . . 5 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
40		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑢∪ 𝑥 ∈ 𝐵 𝐶
41	12, 2	nfiun 5028	. . . . . 6 ⊢ Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶
42	13	iuneq1d 5025	. . . . . 6 ⊢ (𝑦 = 𝑢 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
43	40, 41, 42	cbvdisj 5124	. . . . 5 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
44	39, 43	sylibr 233	. . . 4 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)
45	44	ex 414	. . 3 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))
46	8, 45	jcad 514	. 2 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))
47	14	eleq2i 2826	. . . . . . . 8 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
48		eliun 5002	. . . . . . . 8 ⊢ (𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
49	47, 48	bitri 275	. . . . . . 7 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
50		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑣𝐵
51		nfcsb1v 3919	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐵
52		csbeq1a 3908	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → 𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
53	50, 51, 52	cbviun 5040	. . . . . . . . 9 ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵
54	53	eleq2i 2826	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵)
55		eliun 5002	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
56	54, 55	bitri 275	. . . . . . 7 ⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
57	49, 56	anbi12i 628	. . . . . 6 ⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
58		reeanv 3227	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
59	57, 58	bitr4i 278	. . . . 5 ⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
60		simplrr 777	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠)
61	12, 2	nfdisjw 5126	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶
62	13	disjeq1d 5122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑢 → (Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶))
63	61, 62	rspc 3601	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶))
64	63	impcom 409	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
65		disjors 5130	. . . . . . . . . . . . . . . . 17 ⊢ (Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
66	64, 65	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
67	66	ad2ant2r 746	. . . . . . . . . . . . . . 15 ⊢ (((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
68	67	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
69		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
70		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
71	18	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
72	70, 71	eleqtrrd 2837	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)
73	69, 72	jca 513	. . . . . . . . . . . . . 14 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵))
74		rsp2 3275	. . . . . . . . . . . . . . 15 ⊢ (∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
75	74	imp 408	. . . . . . . . . . . . . 14 ⊢ ((∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
76	68, 73, 75	syl2an2r 684	. . . . . . . . . . . . 13 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
77	76	adantlrr 720	. . . . . . . . . . . 12 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
78	77	ord 863	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
79	60, 78	mpd 15	. . . . . . . . . 10 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
80		ssiun2 5051	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶)
81		nfcv 2904	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟𝐶
82		nfcsb1v 3919	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥⦋𝑟 / 𝑥⦌𝐶
83		csbeq1a 3908	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → 𝐶 = ⦋𝑟 / 𝑥⦌𝐶)
84	81, 82, 83	cbviun 5040	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶
85	80, 84	sseqtrrdi 4034	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
86		ssiun2 5051	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶)
87		nfcv 2904	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑠𝐶
88		nfcsb1v 3919	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐶
89		csbeq1a 3908	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑠 → 𝐶 = ⦋𝑠 / 𝑥⦌𝐶)
90	87, 88, 89	cbviun 5040	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶
91	86, 90	sseqtrrdi 4034	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
92		ss2in 4237	. . . . . . . . . . . . 13 ⊢ ((⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∧ ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
93	85, 91, 92	syl2an 597	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
94	93	ad2antrl 727	. . . . . . . . . . 11 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
95		nfcv 2904	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∪ 𝑥 ∈ 𝐵 𝐶
96		nfcsb1v 3919	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐵
97	96, 2	nfiun 5028	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶
98		csbeq1a 3908	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑦⦌𝐵)
99	98	iuneq1d 5025	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
100	95, 97, 99	cbvdisj 5124	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
101	100	biimpi 215	. . . . . . . . . . . . 13 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
102	101	ad3antlr 730	. . . . . . . . . . . 12 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
103		simplr 768	. . . . . . . . . . . 12 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴))
104		id 22	. . . . . . . . . . . 12 ⊢ (𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣)
105		csbeq1 3897	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑢 / 𝑦⦌𝐵)
106	105	iuneq1d 5025	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
107		csbeq1 3897	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑣 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
108	107	iuneq1d 5025	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
109	106, 108	disji2 5131	. . . . . . . . . . . 12 ⊢ ((Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
110	102, 103, 104, 109	syl2an3an 1423	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
111		sseq0 4400	. . . . . . . . . . 11 ⊢ (((⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) ∧ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
112	94, 110, 111	syl2an2r 684	. . . . . . . . . 10 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
113	79, 112	pm2.61dane 3030	. . . . . . . . 9 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
114	113	expr 458	. . . . . . . 8 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
115	114	orrd 862	. . . . . . 7 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
116	115	ex 414	. . . . . 6 ⊢ (((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
117	116	rexlimdvva 3212	. . . . 5 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
118	59, 117	biimtrid 241	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
119	118	ralrimivv 3199	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ∀𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
120		disjors 5130	. . 3 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ ∀𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
121	119, 120	sylibr 233	. 2 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶)
122	46, 121	impbid1 224	1 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  ⦋csb 3894   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  ∪ ciun 4998  Disj wdisj 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324  df-iun 5000  df-disj 5115

This theorem is referenced by: (None)