Theorem disjxiun 5099

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 4987	. . . . . 6 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝐴 𝐵
2		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑦𝐶
3	1, 2	nfdisjw 5081	. . . . 5 ⊢ Ⅎ𝑦Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶
4		disjss1 5075	. . . . . 6 ⊢ (𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶))
5		ssiun2 5007	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
6	4, 5	syl11 33	. . . . 5 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (𝑦 ∈ 𝐴 → Disj 𝑥 ∈ 𝐵 𝐶))
7	3, 6	ralrimi 3262	. . . 4 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶)
8	7	a1i 11	. . 3 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶))
9		simplr 778	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶)
10		ssiun2 5007	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
11		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑢𝐵
12		nfcsb1v 3878	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑢 / 𝑦⦌𝐵
13		csbeq1a 3868	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑦⦌𝐵)
14	11, 12, 13	cbviun 4994	. . . . . . . . . . . . 13 ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵
15	10, 14	sseqtrrdi 3979	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
16	15	adantr 484	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
17	16	ad2antrl 738	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
18		csbeq1 3857	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑣 → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
19	18	sseq1d 3969	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵))
20	19, 15	vtoclga 3543	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
21	20	adantl 485	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
22	21	ad2antrl 738	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
23	11, 12, 13	cbvdisj 5079	. . . . . . . . . . . . . . . 16 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
24	18	disjor 5084	. . . . . . . . . . . . . . . 16 ⊢ (Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
25	23, 24	sylbb 221	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
26		rsp2 3281	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)))
27	25, 26	syl 17	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)))
28	27	imp 410	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
29	28	ord 875	. . . . . . . . . . . 12 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
30	29	impr 458	. . . . . . . . . . 11 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)
31	30	adantlr 725	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)
32		disjiun 5090	. . . . . . . . . 10 ⊢ ((Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ∧ (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
33	9, 17, 22, 31, 32	syl13anc 1393	. . . . . . . . 9 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
34	33	expr 460	. . . . . . . 8 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
35	34	orrd 874	. . . . . . 7 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
36	35	ralrimivva 3207	. . . . . 6 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
37	18	iuneq1d 4979	. . . . . . 7 ⊢ (𝑢 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
38	37	disjor 5084	. . . . . 6 ⊢ (Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
39	36, 38	sylibr 236	. . . . 5 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
40		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑢∪ 𝑥 ∈ 𝐵 𝐶
41	12, 2	nfiun 4983	. . . . . 6 ⊢ Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶
42	13	iuneq1d 4979	. . . . . 6 ⊢ (𝑦 = 𝑢 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
43	40, 41, 42	cbvdisj 5079	. . . . 5 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
44	39, 43	sylibr 236	. . . 4 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)
45	44	ex 416	. . 3 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))
46	8, 45	jcad 520	. 2 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))
47	14	eleq2i 2856	. . . . . . . 8 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
48		eliun 4955	. . . . . . . 8 ⊢ (𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
49	47, 48	bitri 277	. . . . . . 7 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
50		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑣𝐵
51		nfcsb1v 3878	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐵
52		csbeq1a 3868	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → 𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
53	50, 51, 52	cbviun 4994	. . . . . . . . 9 ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵
54	53	eleq2i 2856	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵)
55		eliun 4955	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
56	54, 55	bitri 277	. . . . . . 7 ⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
57	49, 56	anbi12i 637	. . . . . 6 ⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
58		reeanv 3236	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
59	57, 58	bitr4i 280	. . . . 5 ⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
60	12, 2	nfdisjw 5081	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶
61	13	disjeq1d 5077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑢 → (Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶))
62	60, 61	rspc 3571	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶))
63	62	impcom 411	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
64		disjors 5085	. . . . . . . . . . . . . . . 16 ⊢ (Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
65	63, 64	sylib 220	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
66	65	ad2ant2r 757	. . . . . . . . . . . . . 14 ⊢ (((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
67	66	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
68		simplrl 786	. . . . . . . . . . . . . 14 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
69		simplrr 787	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
70	18	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
71	69, 70	eleqtrrd 2867	. . . . . . . . . . . . . 14 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)
72	68, 71	jca 519	. . . . . . . . . . . . 13 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵))
73		rsp2 3281	. . . . . . . . . . . . . 14 ⊢ (∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
74	73	imp 410	. . . . . . . . . . . . 13 ⊢ ((∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
75	67, 72, 74	syl2an2r 695	. . . . . . . . . . . 12 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
76	75	adantlrr 731	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
77		simplrr 787	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠)
78	76, 77	orcnd 889	. . . . . . . . . 10 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
79		ssiun2 5007	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶)
80		nfcv 2926	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟𝐶
81		nfcsb1v 3878	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥⦋𝑟 / 𝑥⦌𝐶
82		csbeq1a 3868	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → 𝐶 = ⦋𝑟 / 𝑥⦌𝐶)
83	80, 81, 82	cbviun 4994	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶
84	79, 83	sseqtrrdi 3979	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
85		ssiun2 5007	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶)
86		nfcv 2926	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑠𝐶
87		nfcsb1v 3878	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐶
88		csbeq1a 3868	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑠 → 𝐶 = ⦋𝑠 / 𝑥⦌𝐶)
89	86, 87, 88	cbviun 4994	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶
90	85, 89	sseqtrrdi 3979	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
91		ss2in 4198	. . . . . . . . . . . . 13 ⊢ ((⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∧ ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
92	84, 90, 91	syl2an 605	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
93	92	ad2antrl 738	. . . . . . . . . . 11 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
94		nfcv 2926	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∪ 𝑥 ∈ 𝐵 𝐶
95		nfcsb1v 3878	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐵
96	95, 2	nfiun 4983	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶
97		csbeq1a 3868	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑦⦌𝐵)
98	97	iuneq1d 4979	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
99	94, 96, 98	cbvdisj 5079	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
100	99	biimpi 218	. . . . . . . . . . . . 13 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
101	100	ad3antlr 741	. . . . . . . . . . . 12 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
102		simplr 778	. . . . . . . . . . . 12 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴))
103		id 22	. . . . . . . . . . . 12 ⊢ (𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣)
104		csbeq1 3857	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑢 / 𝑦⦌𝐵)
105	104	iuneq1d 4979	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
106		csbeq1 3857	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑣 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
107	106	iuneq1d 4979	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
108	105, 107	disji2 5086	. . . . . . . . . . . 12 ⊢ ((Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
109	101, 102, 103, 108	syl2an3an 1443	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
110		sseq0 4359	. . . . . . . . . . 11 ⊢ (((⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) ∧ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
111	93, 109, 110	syl2an2r 695	. . . . . . . . . 10 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
112	78, 111	pm2.61dane 3046	. . . . . . . . 9 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
113	112	expr 460	. . . . . . . 8 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
114	113	orrd 874	. . . . . . 7 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
115	114	ex 416	. . . . . 6 ⊢ (((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
116	115	rexlimdvva 3221	. . . . 5 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
117	59, 116	biimtrid 244	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
118	117	ralrimivv 3205	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ∀𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
119		disjors 5085	. . 3 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ ∀𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
120	118, 119	sylibr 236	. 2 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶)
121	46, 120	impbid1 227	1 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1562   ∈ wcel 2144   ≠ wne 2959  ∀wral 3078  ∃wrex 3088  ⦋csb 3854   ∩ cin 3905   ⊆ wss 3906  ∅c0 4287  ∪ ciun 4951  Disj wdisj 5069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rmo 3369  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-in 3913  df-ss 3923  df-nul 4288  df-iun 4953  df-disj 5070

This theorem is referenced by: (None)