Metamath Proof Explorer

Theorem iundisj2f

Description: A disjoint union is disjoint. Cf. iundisj2 . (Contributed by Thierry Arnoux, 30-Dec-2016)

Ref Expression
Hypotheses iundisjf.1 ⊢ Ⅎ 𝑘 𝐴
iundisjf.2 ⊢ Ⅎ 𝑛 𝐵
iundisjf.3 ⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
Assertion iundisj2f Disj 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )

Proof

Step Hyp Ref Expression
1 iundisjf.1 ⊢ Ⅎ 𝑘 𝐴
2 iundisjf.2 ⊢ Ⅎ 𝑛 𝐵
3 iundisjf.3 ⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
4 tru ⊢ ⊤
5 eqeq12 ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( 𝑎 = 𝑏 ↔ 𝑥 = 𝑦 ) )
6 csbeq1 ⊢ ( 𝑎 = 𝑥 → ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
7 csbeq1 ⊢ ( 𝑏 = 𝑦 → ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
8 6 7 ineqan12d ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
9 8 eqeq1d ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ↔ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
10 5 9 orbi12d ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( 𝑎 = 𝑏 ∨ ( ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) ↔ ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) ) )
11 eqeq12 ⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( 𝑎 = 𝑏 ↔ 𝑦 = 𝑥 ) )
12 equcom ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
13 11 12 bitrdi ⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( 𝑎 = 𝑏 ↔ 𝑥 = 𝑦 ) )
14 csbeq1 ⊢ ( 𝑎 = 𝑦 → ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
15 csbeq1 ⊢ ( 𝑏 = 𝑥 → ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
16 14 15 ineqan12d ⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ( ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
17 incom ⊢ ( ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
18 16 17 eqtrdi ⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
19 18 eqeq1d ⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( ( ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ↔ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
20 13 19 orbi12d ⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( ( 𝑎 = 𝑏 ∨ ( ⦋ 𝑎 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑏 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) ↔ ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) ) )
21 nnssre ⊢ ℕ ⊆ ℝ
22 21 a1i ⊢ ( ⊤ → ℕ ⊆ ℝ )
23 biidd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) → ( ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) ↔ ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) ) )
24 nesym ⊢ ( 𝑦 ≠ 𝑥 ↔ ¬ 𝑥 = 𝑦 )
25 nnre ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
26 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
27 id ⊢ ( 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝑦 )
28 leltne ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) → ( 𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥 ) )
29 25 26 27 28 syl3an ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦 ) → ( 𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥 ) )
30 vex ⊢ 𝑥 ∈ V
31 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑥 / 𝑛 ⦌ 𝐴
32 nfcv ⊢ Ⅎ 𝑛 ( 1 ..^ 𝑥 )
33 32 2 nfiun ⊢ Ⅎ 𝑛 ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵
34 31 33 nfdif ⊢ Ⅎ 𝑛 ( ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵 )
35 csbeq1a ⊢ ( 𝑛 = 𝑥 → 𝐴 = ⦋ 𝑥 / 𝑛 ⦌ 𝐴 )
36 oveq2 ⊢ ( 𝑛 = 𝑥 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑥 ) )
37 36 iuneq1d ⊢ ( 𝑛 = 𝑥 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵 )
38 35 37 difeq12d ⊢ ( 𝑛 = 𝑥 → ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ( ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵 ) )
39 30 34 38 csbief ⊢ ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ( ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵 )
40 vex ⊢ 𝑦 ∈ V
41 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑦 / 𝑛 ⦌ 𝐴
42 nfcv ⊢ Ⅎ 𝑛 ( 1 ..^ 𝑦 )
43 42 2 nfiun ⊢ Ⅎ 𝑛 ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵
44 41 43 nfdif ⊢ Ⅎ 𝑛 ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 )
45 csbeq1a ⊢ ( 𝑛 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑛 ⦌ 𝐴 )
46 oveq2 ⊢ ( 𝑛 = 𝑦 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑦 ) )
47 46 iuneq1d ⊢ ( 𝑛 = 𝑦 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 )
48 45 47 difeq12d ⊢ ( 𝑛 = 𝑦 → ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) )
49 40 44 48 csbief ⊢ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 )
50 39 49 ineq12i ⊢ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ( ( ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵 ) ∩ ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) )
51 simp1 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℕ )
52 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
53 51 52 eleqtrdi ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( ℤ≥ ‘ 1 ) )
54 simp2 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℕ )
55 54 nnzd ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℤ )
56 simp3 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
57 elfzo2 ⊢ ( 𝑥 ∈ ( 1 ..^ 𝑦 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑦 ∈ ℤ ∧ 𝑥 < 𝑦 ) )
58 53 55 56 57 syl3anbrc ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 1 ..^ 𝑦 ) )
59 nfcv ⊢ Ⅎ 𝑘 ( 1 ..^ 𝑦 )
60 nfcv ⊢ Ⅎ 𝑘 𝑥
61 60 1 nfcsbw ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑛 ⦌ 𝐴
62 nfcv ⊢ Ⅎ 𝑛 𝑘
63 62 2 3 csbhypf ⊢ ( 𝑥 = 𝑘 → ⦋ 𝑥 / 𝑛 ⦌ 𝐴 = 𝐵 )
64 63 equcoms ⊢ ( 𝑘 = 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ 𝐴 = 𝐵 )
65 64 eqcomd ⊢ ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑥 / 𝑛 ⦌ 𝐴 )
66 59 60 61 65 ssiun2sf ⊢ ( 𝑥 ∈ ( 1 ..^ 𝑦 ) → ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ⊆ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 )
67 58 66 syl ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ⊆ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 )
68 67 ssdifssd ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → ( ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵 ) ⊆ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 )
69 68 ssrind ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → ( ( ⦋ 𝑥 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑥 ) 𝐵 ) ∩ ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) ) ⊆ ( ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ∩ ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) ) )
70 50 69 eqsstrid ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) ⊆ ( ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ∩ ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) ) )
71 disjdif ⊢ ( ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ∩ ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) ) = ∅
72 sseq0 ⊢ ( ( ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) ⊆ ( ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ∩ ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) ) ∧ ( ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ∩ ( ⦋ 𝑦 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑦 ) 𝐵 ) ) = ∅ ) → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ )
73 70 71 72 sylancl ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦 ) → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ )
74 73 3expia ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 < 𝑦 → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
75 74 3adant3 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦 ) → ( 𝑥 < 𝑦 → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
76 29 75 sylbird ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦 ) → ( 𝑦 ≠ 𝑥 → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
77 24 76 syl5bir ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦 ) → ( ¬ 𝑥 = 𝑦 → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
78 77 orrd ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦 ) → ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
79 78 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦 ) ) → ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
80 10 20 22 23 79 wlogle ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
81 4 80 mpan ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
82 81 rgen2 ⊢ ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ ℕ ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ )
83 disjors ⊢ ( Disj 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ↔ ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ ℕ ( 𝑥 = 𝑦 ∨ ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ∩ ⦋ 𝑦 / 𝑛 ⦌ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) = ∅ ) )
84 82 83 mpbir ⊢ Disj 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )