Theorem disjxiun 4649

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 4550	. . . . . 6 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝐴 𝐵
2		nfcv 2764	. . . . . 6 ⊢ Ⅎ𝑦𝐶
3	1, 2	nfdisj 4632	. . . . 5 ⊢ Ⅎ𝑦Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶
4		disjss1 4626	. . . . . 6 ⊢ (𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑥 ∈ 𝐵 𝐶))
5		ssiun2 4563	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
6	4, 5	syl11 33	. . . . 5 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (𝑦 ∈ 𝐴 → Disj 𝑥 ∈ 𝐵 𝐶))
7	3, 6	ralrimi 2957	. . . 4 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶)
8	7	a1i 11	. . 3 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → ∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶))
9		simplr 792	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶)
10		ssiun2 4563	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
11		nfcv 2764	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑢𝐵
12		nfcsb1v 3549	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑢 / 𝑦⦌𝐵
13		csbeq1a 3542	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑦⦌𝐵)
14	11, 12, 13	cbviun 4557	. . . . . . . . . . . . 13 ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵
15	10, 14	syl6sseqr 3652	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝐴 → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
16	15	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
17	16	ad2antrl 764	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
18		csbeq1 3536	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑣 → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
19	18	sseq1d 3632	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵))
20	19, 15	vtoclga 3272	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
21	20	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
22	21	ad2antrl 764	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵)
23	11, 12, 13	cbvdisj 4630	. . . . . . . . . . . . . . . 16 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
24	18	disjor 4634	. . . . . . . . . . . . . . . 16 ⊢ (Disj 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
25	23, 24	sylbb 209	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
26		rsp2 2936	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)))
27	25, 26	syl 17	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)))
28	27	imp 445	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
29	28	ord 392	. . . . . . . . . . . 12 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅))
30	29	impr 649	. . . . . . . . . . 11 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)
31	30	adantlr 751	. . . . . . . . . 10 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)
32		disjiun 4640	. . . . . . . . . 10 ⊢ ((Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ∧ (⦋𝑢 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ ⦋𝑣 / 𝑦⦌𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ (⦋𝑢 / 𝑦⦌𝐵 ∩ ⦋𝑣 / 𝑦⦌𝐵) = ∅)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
33	9, 17, 22, 31, 32	syl13anc 1328	. . . . . . . . 9 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ¬ 𝑢 = 𝑣)) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
34	33	expr 643	. . . . . . . 8 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (¬ 𝑢 = 𝑣 → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
35	34	orrd 393	. . . . . . 7 ⊢ (((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
36	35	ralrimivva 2971	. . . . . 6 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
37	18	iuneq1d 4545	. . . . . . 7 ⊢ (𝑢 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
38	37	disjor 4634	. . . . . 6 ⊢ (Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅))
39	36, 38	sylibr 224	. . . . 5 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
40		nfcv 2764	. . . . . 6 ⊢ Ⅎ𝑢∪ 𝑥 ∈ 𝐵 𝐶
41	12, 2	nfiun 4548	. . . . . 6 ⊢ Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶
42	13	iuneq1d 4545	. . . . . 6 ⊢ (𝑦 = 𝑢 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
43	40, 41, 42	cbvdisj 4630	. . . . 5 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
44	39, 43	sylibr 224	. . . 4 ⊢ ((Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)
45	44	ex 450	. . 3 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))
46	8, 45	jcad 555	. 2 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))
47	14	eleq2i 2693	. . . . . . . 8 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵)
48		eliun 4524	. . . . . . . 8 ⊢ (𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋𝑢 / 𝑦⦌𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
49	47, 48	bitri 264	. . . . . . 7 ⊢ (𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
50		nfcv 2764	. . . . . . . . . 10 ⊢ Ⅎ𝑣𝐵
51		nfcsb1v 3549	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐵
52		csbeq1a 3542	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → 𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
53	50, 51, 52	cbviun 4557	. . . . . . . . 9 ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵
54	53	eleq2i 2693	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵)
55		eliun 4524	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋𝑣 / 𝑦⦌𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
56	54, 55	bitri 264	. . . . . . 7 ⊢ (𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
57	49, 56	anbi12i 733	. . . . . 6 ⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
58		reeanv 3107	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ↔ (∃𝑢 ∈ 𝐴 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ ∃𝑣 ∈ 𝐴 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
59	57, 58	bitr4i 267	. . . . 5 ⊢ ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵))
60		simplrr 801	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠)
61	12, 2	nfdisj 4632	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶
62	13	disjeq1d 4628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑢 → (Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶))
63	61, 62	rspc 3303	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶))
64	63	impcom 446	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
65		disjors 4635	. . . . . . . . . . . . . . . . 17 ⊢ (Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ↔ ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
66	64, 65	sylib 208	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
67	66	ad2ant2r 783	. . . . . . . . . . . . . . 15 ⊢ (((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
68	67	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → ∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
69		simplrl 800	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵)
70		simplrr 801	. . . . . . . . . . . . . . . 16 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)
71	18	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → ⦋𝑢 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
72	70, 71	eleqtrrd 2704	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)
73	69, 72	jca 554	. . . . . . . . . . . . . 14 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵))
74		rsp2 2936	. . . . . . . . . . . . . . 15 ⊢ (∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
75	74	imp 445	. . . . . . . . . . . . . 14 ⊢ ((∀𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵∀𝑠 ∈ ⦋ 𝑢 / 𝑦⦌𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑢 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
76	68, 73, 75	syl2an2r 876	. . . . . . . . . . . . 13 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
77	76	adantlrr 757	. . . . . . . . . . . 12 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
78	77	ord 392	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
79	60, 78	mpd 15	. . . . . . . . . 10 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
80		ssiun2 4563	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶)
81		nfcv 2764	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟𝐶
82		nfcsb1v 3549	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥⦋𝑟 / 𝑥⦌𝐶
83		csbeq1a 3542	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → 𝐶 = ⦋𝑟 / 𝑥⦌𝐶)
84	81, 82, 83	cbviun 4557	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦⦌𝐵⦋𝑟 / 𝑥⦌𝐶
85	80, 84	syl6sseqr 3652	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 → ⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
86		ssiun2 4563	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶)
87		nfcv 2764	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑠𝐶
88		nfcsb1v 3549	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐶
89		csbeq1a 3542	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑠 → 𝐶 = ⦋𝑠 / 𝑥⦌𝐶)
90	87, 88, 89	cbviun 4557	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦⦌𝐵⦋𝑠 / 𝑥⦌𝐶
91	86, 90	syl6sseqr 3652	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵 → ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
92		ss2in 3840	. . . . . . . . . . . . 13 ⊢ ((⦋𝑟 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∧ ⦋𝑠 / 𝑥⦌𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
93	85, 91, 92	syl2an 494	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
94	93	ad2antrl 764	. . . . . . . . . . 11 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶))
95		nfcv 2764	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∪ 𝑥 ∈ 𝐵 𝐶
96		nfcsb1v 3549	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐵
97	96, 2	nfiun 4548	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶
98		csbeq1a 3542	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑦⦌𝐵)
99	98	iuneq1d 4545	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
100	95, 97, 99	cbvdisj 4630	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
101	100	biimpi 206	. . . . . . . . . . . . 13 ⊢ (Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
102	101	ad3antlr 767	. . . . . . . . . . . 12 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶)
103		simplr 792	. . . . . . . . . . . 12 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴))
104		id 22	. . . . . . . . . . . 12 ⊢ (𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣)
105		csbeq1 3536	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑢 / 𝑦⦌𝐵)
106	105	iuneq1d 4545	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶)
107		csbeq1 3536	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑣 → ⦋𝑧 / 𝑦⦌𝐵 = ⦋𝑣 / 𝑦⦌𝐵)
108	107	iuneq1d 4545	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶)
109	106, 108	disji2 4636	. . . . . . . . . . . 12 ⊢ ((Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦⦌𝐵𝐶 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
110	102, 103, 104, 109	syl2an3an 1386	. . . . . . . . . . 11 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅)
111		sseq0 3975	. . . . . . . . . . 11 ⊢ (((⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) ⊆ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) ∧ (∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦⦌𝐵𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦⦌𝐵𝐶) = ∅) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
112	94, 110, 111	syl2an2r 876	. . . . . . . . . 10 ⊢ (((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 ≠ 𝑣) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
113	79, 112	pm2.61dane 2881	. . . . . . . . 9 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) ∧ ¬ 𝑟 = 𝑠)) → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)
114	113	expr 643	. . . . . . . 8 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (¬ 𝑟 = 𝑠 → (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
115	114	orrd 393	. . . . . . 7 ⊢ ((((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) ∧ (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵)) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
116	115	ex 450	. . . . . 6 ⊢ (((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
117	116	rexlimdvva 3038	. . . . 5 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ 𝐴 (𝑟 ∈ ⦋𝑢 / 𝑦⦌𝐵 ∧ 𝑠 ∈ ⦋𝑣 / 𝑦⦌𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
118	59, 117	syl5bi 232	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ((𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) → (𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅)))
119	118	ralrimivv 2970	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → ∀𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
120		disjors 4635	. . 3 ⊢ (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ ∀𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵∀𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵(𝑟 = 𝑠 ∨ (⦋𝑟 / 𝑥⦌𝐶 ∩ ⦋𝑠 / 𝑥⦌𝐶) = ∅))
121	119, 120	sylibr 224	. 2 ⊢ ((∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶)
122	46, 121	impbid1 215	1 ⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  ⦋csb 3533   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  ∪ ciun 4520  Disj wdisj 4620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-iun 4522  df-disj 4621

This theorem is referenced by: (None)