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

Metamath Proof Explorer

Theorem iundisj2

Description: A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis iundisj.1 ⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
Assertion iundisj2 Disj 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )

Proof

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