Metamath Proof Explorer

Theorem iundisj2fi

Description: A disjoint union is disjoint, finite version. Cf. iundisj2 . (Contributed by Thierry Arnoux, 16-Feb-2017)

Ref Expression
Hypotheses iundisj2fi.0 ⊢ Ⅎ 𝑛 𝐵
iundisj2fi.1 ⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
Assertion iundisj2fi Disj 𝑛 ∈ ( 1 ..^ 𝑁 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )

Proof

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