Metamath Proof Explorer

Theorem 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 ( Disj 𝑦 ∈ 𝐴 𝐵 → ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ↔ ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ 𝐴 𝐵
2 nfcv ⊢ Ⅎ 𝑦 𝐶
3 1 2 nfdisjw ⊢ Ⅎ 𝑦 Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶
4 disjss1 ⊢ ( 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 → ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 𝐶 ) )
5 ssiun2 ⊢ ( 𝑦 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 )
6 4 5 syl11 ⊢ ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 → ( 𝑦 ∈ 𝐴 → Disj 𝑥 ∈ 𝐵 𝐶 ) )
7 3 6 ralrimi ⊢ ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 → ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 )
8 7 a1i ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 → ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 → ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ) )
9 simplr ⊢ ( ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ¬ 𝑢 = 𝑣 ) ) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 )
10 ssiun2 ⊢ ( 𝑢 ∈ 𝐴 → ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑢 ∈ 𝐴 ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
11 nfcv ⊢ Ⅎ 𝑢 𝐵
12 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑢 / 𝑦 ⦌ 𝐵
13 csbeq1a ⊢ ( 𝑦 = 𝑢 → 𝐵 = ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
14 11 12 13 cbviun ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑢 ∈ 𝐴 ⦋ 𝑢 / 𝑦 ⦌ 𝐵
15 10 14 sseqtrrdi ⊢ ( 𝑢 ∈ 𝐴 → ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 )
16 15 adantr ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 )
17 16 ad2antrl ⊢ ( ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ¬ 𝑢 = 𝑣 ) ) → ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 )
18 csbeq1 ⊢ ( 𝑢 = 𝑣 → ⦋ 𝑢 / 𝑦 ⦌ 𝐵 = ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
19 18 sseq1d ⊢ ( 𝑢 = 𝑣 → ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ) )
20 19 15 vtoclga ⊢ ( 𝑣 ∈ 𝐴 → ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 )
21 20 adantl ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 )
22 21 ad2antrl ⊢ ( ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ¬ 𝑢 = 𝑣 ) ) → ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 )
23 11 12 13 cbvdisj ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 ↔ Disj 𝑢 ∈ 𝐴 ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
24 18 disjor ⊢ ( Disj 𝑢 ∈ 𝐴 ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) )
25 23 24 sylbb ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) )
26 rsp2 ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 = 𝑣 ∨ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) ) )
27 25 26 syl ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 = 𝑣 ∨ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) ) )
28 27 imp ⊢ ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 = 𝑣 ∨ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) )
29 28 ord ⊢ ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ¬ 𝑢 = 𝑣 → ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) )
30 29 impr ⊢ ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ¬ 𝑢 = 𝑣 ) ) → ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ )
31 30 adantlr ⊢ ( ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ¬ 𝑢 = 𝑣 ) ) → ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ )
32 disjiun ⊢ ( ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ∧ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⊆ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ ( ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∩ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) = ∅ ) ) → ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ )
33 9 17 22 31 32 syl13anc ⊢ ( ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ¬ 𝑢 = 𝑣 ) ) → ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ )
34 33 expr ⊢ ( ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ¬ 𝑢 = 𝑣 → ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ ) )
35 34 orrd ⊢ ( ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 = 𝑣 ∨ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ ) )
36 35 ralrimivva ⊢ ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ ) )
37 18 iuneq1d ⊢ ( 𝑢 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 )
38 37 disjor ⊢ ( Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ ) )
39 36 38 sylibr ⊢ ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) → Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
40 nfcv ⊢ Ⅎ 𝑢 ∪ 𝑥 ∈ 𝐵 𝐶
41 12 2 nfiun ⊢ Ⅎ 𝑦 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶
42 13 iuneq1d ⊢ ( 𝑦 = 𝑢 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
43 40 41 42 cbvdisj ⊢ ( Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
44 39 43 sylibr ⊢ ( ( Disj 𝑦 ∈ 𝐴 𝐵 ∧ Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ) → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 )
45 44 ex ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 → ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 → Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) )
46 8 45 jcad ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 → ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 → ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ) )
47 14 eleq2i ⊢ ( 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
48 eliun ⊢ ( 𝑟 ∈ ∪ 𝑢 ∈ 𝐴 ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ↔ ∃ 𝑢 ∈ 𝐴 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
49 47 48 bitri ⊢ ( 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃ 𝑢 ∈ 𝐴 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
50 nfcv ⊢ Ⅎ 𝑣 𝐵
51 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ 𝐵
52 csbeq1a ⊢ ( 𝑦 = 𝑣 → 𝐵 = ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
53 50 51 52 cbviun ⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = ∪ 𝑣 ∈ 𝐴 ⦋ 𝑣 / 𝑦 ⦌ 𝐵
54 53 eleq2i ⊢ ( 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ 𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
55 eliun ⊢ ( 𝑠 ∈ ∪ 𝑣 ∈ 𝐴 ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ↔ ∃ 𝑣 ∈ 𝐴 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
56 54 55 bitri ⊢ ( 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃ 𝑣 ∈ 𝐴 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
57 49 56 anbi12i ⊢ ( ( 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ) ↔ ( ∃ 𝑢 ∈ 𝐴 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ ∃ 𝑣 ∈ 𝐴 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) )
58 reeanv ⊢ ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ↔ ( ∃ 𝑢 ∈ 𝐴 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ ∃ 𝑣 ∈ 𝐴 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) )
59 57 58 bitr4i ⊢ ( ( 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) )
60 simplrr ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 = 𝑣 ) → ¬ 𝑟 = 𝑠 )
61 12 2 nfdisjw ⊢ Ⅎ 𝑦 Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶
62 13 disjeq1d ⊢ ( 𝑦 = 𝑢 → ( Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ) )
63 61 62 rspc ⊢ ( 𝑢 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ) )
64 63 impcom ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴 ) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
65 disjors ⊢ ( Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ↔ ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
66 64 65 sylib ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴 ) → ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
67 66 ad2ant2r ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
68 67 adantr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) → ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
69 simplrl ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
70 simplrr ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
71 18 adantl ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → ⦋ 𝑢 / 𝑦 ⦌ 𝐵 = ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
72 70 71 eleqtrrd ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
73 69 72 jca ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ) )
74 rsp2 ⊢ ( ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) → ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
75 74 imp ⊢ ( ( ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ) ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
76 68 73 75 syl2an2r ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
77 76 adantlrr ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 = 𝑣 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
78 77 ord ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 = 𝑣 ) → ( ¬ 𝑟 = 𝑠 → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
79 60 78 mpd ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 = 𝑣 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
80 ssiun2 ⊢ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 → ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⦋ 𝑟 / 𝑥 ⦌ 𝐶 )
81 nfcv ⊢ Ⅎ 𝑟 𝐶
82 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑟 / 𝑥 ⦌ 𝐶
83 csbeq1a ⊢ ( 𝑥 = 𝑟 → 𝐶 = ⦋ 𝑟 / 𝑥 ⦌ 𝐶 )
84 81 82 83 cbviun ⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⦋ 𝑟 / 𝑥 ⦌ 𝐶
85 80 84 sseqtrrdi ⊢ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 → ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
86 ssiun2 ⊢ ( 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 → ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⦋ 𝑠 / 𝑥 ⦌ 𝐶 )
87 nfcv ⊢ Ⅎ 𝑠 𝐶
88 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐶
89 csbeq1a ⊢ ( 𝑥 = 𝑠 → 𝐶 = ⦋ 𝑠 / 𝑥 ⦌ 𝐶 )
90 87 88 89 cbviun ⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⦋ 𝑠 / 𝑥 ⦌ 𝐶
91 86 90 sseqtrrdi ⊢ ( 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 → ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 )
92 ss2in ⊢ ( ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∧ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) )
93 85 91 92 syl2an ⊢ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) )
94 93 ad2antrl ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) )
95 nfcv ⊢ Ⅎ 𝑧 ∪ 𝑥 ∈ 𝐵 𝐶
96 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐵
97 96 2 nfiun ⊢ Ⅎ 𝑦 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶
98 csbeq1a ⊢ ( 𝑦 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑦 ⦌ 𝐵 )
99 98 iuneq1d ⊢ ( 𝑦 = 𝑧 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
100 95 97 99 cbvdisj ⊢ ( Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
101 100 biimpi ⊢ ( Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
102 101 ad3antlr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
103 simplr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
104 id ⊢ ( 𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣 )
105 csbeq1 ⊢ ( 𝑧 = 𝑢 → ⦋ 𝑧 / 𝑦 ⦌ 𝐵 = ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
106 105 iuneq1d ⊢ ( 𝑧 = 𝑢 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
107 csbeq1 ⊢ ( 𝑧 = 𝑣 → ⦋ 𝑧 / 𝑦 ⦌ 𝐵 = ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
108 107 iuneq1d ⊢ ( 𝑧 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 )
109 106 108 disji2 ⊢ ( ( Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑢 ≠ 𝑣 ) → ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ )
110 102 103 104 109 syl2an3an ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ )
111 sseq0 ⊢ ( ( ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) ∧ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
112 94 110 111 syl2an2r ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
113 79 112 pm2.61dane ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
114 113 expr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) → ( ¬ 𝑟 = 𝑠 → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
115 114 orrd ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
116 115 ex ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
117 116 rexlimdvva ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
118 59 117 syl5bi ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → ( ( 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
119 118 ralrimivv ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → ∀ 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
120 disjors ⊢ ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ↔ ∀ 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
121 119 120 sylibr ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 )
122 46 121 impbid1 ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 → ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ↔ ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ) )