This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 12 2 nfdisjw ⊢ Ⅎ 𝑦 Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶
61 13 disjeq1d ⊢ ( 𝑦 = 𝑢 → ( Disj 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ) )
62 60 61 rspc ⊢ ( 𝑢 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ) )
63 62 impcom ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴 ) → Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
64 disjors ⊢ ( Disj 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ↔ ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
65 63 64 sylib ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ 𝑢 ∈ 𝐴 ) → ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
66 65 ad2ant2r ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
67 66 adantr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) → ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
68 simplrl ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
69 simplrr ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
70 18 adantl ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → ⦋ 𝑢 / 𝑦 ⦌ 𝐵 = ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
71 69 70 eleqtrrd ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
72 68 71 jca ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ) )
73 rsp2 ⊢ ( ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) → ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
74 73 imp ⊢ ( ( ∀ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∀ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ) ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
75 67 72 74 syl2an2r ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) ∧ 𝑢 = 𝑣 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
76 75 adantlrr ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 = 𝑣 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
77 simplrr ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 = 𝑣 ) → ¬ 𝑟 = 𝑠 )
78 76 77 orcnd ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 = 𝑣 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
79 ssiun2 ⊢ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 → ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⦋ 𝑟 / 𝑥 ⦌ 𝐶 )
80 nfcv ⊢ Ⅎ 𝑟 𝐶
81 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑟 / 𝑥 ⦌ 𝐶
82 csbeq1a ⊢ ( 𝑥 = 𝑟 → 𝐶 = ⦋ 𝑟 / 𝑥 ⦌ 𝐶 )
83 80 81 82 cbviun ⊢ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ⦋ 𝑟 / 𝑥 ⦌ 𝐶
84 79 83 sseqtrrdi ⊢ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 → ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
85 ssiun2 ⊢ ( 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 → ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⦋ 𝑠 / 𝑥 ⦌ 𝐶 )
86 nfcv ⊢ Ⅎ 𝑠 𝐶
87 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐶
88 csbeq1a ⊢ ( 𝑥 = 𝑠 → 𝐶 = ⦋ 𝑠 / 𝑥 ⦌ 𝐶 )
89 86 87 88 cbviun ⊢ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ⦋ 𝑠 / 𝑥 ⦌ 𝐶
90 85 89 sseqtrrdi ⊢ ( 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 → ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 )
91 ss2in ⊢ ( ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∧ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ⊆ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) )
92 84 90 91 syl2an ⊢ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) )
93 92 ad2antrl ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) )
94 nfcv ⊢ Ⅎ 𝑧 ∪ 𝑥 ∈ 𝐵 𝐶
95 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐵
96 95 2 nfiun ⊢ Ⅎ 𝑦 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶
97 csbeq1a ⊢ ( 𝑦 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑦 ⦌ 𝐵 )
98 97 iuneq1d ⊢ ( 𝑦 = 𝑧 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
99 94 96 98 cbvdisj ⊢ ( Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
100 99 biimpi ⊢ ( Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
101 100 ad3antlr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 )
102 simplr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
103 id ⊢ ( 𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣 )
104 csbeq1 ⊢ ( 𝑧 = 𝑢 → ⦋ 𝑧 / 𝑦 ⦌ 𝐵 = ⦋ 𝑢 / 𝑦 ⦌ 𝐵 )
105 104 iuneq1d ⊢ ( 𝑧 = 𝑢 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 )
106 csbeq1 ⊢ ( 𝑧 = 𝑣 → ⦋ 𝑧 / 𝑦 ⦌ 𝐵 = ⦋ 𝑣 / 𝑦 ⦌ 𝐵 )
107 106 iuneq1d ⊢ ( 𝑧 = 𝑣 → ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 = ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 )
108 105 107 disji2 ⊢ ( ( Disj 𝑧 ∈ 𝐴 ∪ 𝑥 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐵 𝐶 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑢 ≠ 𝑣 ) → ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ )
109 101 102 103 108 syl2an3an ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ )
110 sseq0 ⊢ ( ( ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) ⊆ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) ∧ ( ∪ 𝑥 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 𝐶 ) = ∅ ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
111 93 109 110 syl2an2r ⊢ ( ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
112 78 111 pm2.61dane ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ∧ ¬ 𝑟 = 𝑠 ) ) → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ )
113 112 expr ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) → ( ¬ 𝑟 = 𝑠 → ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
114 113 orrd ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
115 114 ex ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
116 115 rexlimdvva ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ( 𝑟 ∈ ⦋ 𝑢 / 𝑦 ⦌ 𝐵 ∧ 𝑠 ∈ ⦋ 𝑣 / 𝑦 ⦌ 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
117 59 116 biimtrid ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → ( ( 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ) → ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) ) )
118 117 ralrimivv ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → ∀ 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
119 disjors ⊢ ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ↔ ∀ 𝑟 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ( 𝑟 = 𝑠 ∨ ( ⦋ 𝑟 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝑠 / 𝑥 ⦌ 𝐶 ) = ∅ ) )
120 118 119 sylibr ⊢ ( ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) → Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 )
121 46 120 impbid1 ⊢ ( Disj 𝑦 ∈ 𝐴 𝐵 → ( Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ↔ ( ∀ 𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ) ) )