Metamath Proof Explorer

Theorem iundisjfi

Description: Rewrite a countable union as a disjoint union, finite version. Cf. iundisj . (Contributed by Thierry Arnoux, 15-Feb-2017)

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

Proof

Step Hyp Ref Expression
1 iundisj3.0 ⊢ Ⅎ 𝑛 𝐵
2 iundisj3.1 ⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
3 ssrab2 ⊢ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ⊆ ( 1 ..^ 𝑁 )
4 fzossnn ⊢ ( 1 ..^ 𝑁 ) ⊆ ℕ
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 4 5 sseqtri ⊢ ( 1 ..^ 𝑁 ) ⊆ ( ℤ≥ ‘ 1 )
7 3 6 sstri ⊢ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ⊆ ( ℤ≥ ‘ 1 )
8 rabn0 ⊢ ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ≠ ∅ ↔ ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 )
9 8 biimpri ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ≠ ∅ )
10 infssuzcl ⊢ ( ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ≠ ∅ ) → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } )
11 7 9 10 sylancr ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } )
12 3 11 sselid ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ( 1 ..^ 𝑁 ) )
13 nfrab1 ⊢ Ⅎ 𝑛 { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 }
14 nfcv ⊢ Ⅎ 𝑛 ℝ
15 nfcv ⊢ Ⅎ 𝑛 <
16 13 14 15 nfinf ⊢ Ⅎ 𝑛 inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < )
17 nfcv ⊢ Ⅎ 𝑛 ( 1 ..^ 𝑁 )
18 16 nfcsb1 ⊢ Ⅎ 𝑛 ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴
19 18 nfcri ⊢ Ⅎ 𝑛 𝑥 ∈ ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴
20 csbeq1a ⊢ ( 𝑛 = inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) → 𝐴 = ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 )
21 20 eleq2d ⊢ ( 𝑛 = inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 ) )
22 16 17 19 21 elrabf ⊢ ( inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ↔ ( inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 ∈ ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 ) )
23 11 22 sylib ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ( inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 ∈ ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 ) )
24 23 simprd ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → 𝑥 ∈ ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 )
25 3 4 sstri ⊢ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ⊆ ℕ
26 nnssre ⊢ ℕ ⊆ ℝ
27 25 26 sstri ⊢ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ⊆ ℝ
28 27 11 sselid ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
29 28 ltnrd ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ¬ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) < inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) )
30 eliun ⊢ ( 𝑥 ∈ ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 ↔ ∃ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝑥 ∈ 𝐵 )
31 28 ad2antrr ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
32 elfzouz2 ⊢ ( inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ( 1 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) )
33 fzoss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) → ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ⊆ ( 1 ..^ 𝑁 ) )
34 12 32 33 3syl ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ⊆ ( 1 ..^ 𝑁 ) )
35 34 sselda ⊢ ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) → 𝑘 ∈ ( 1 ..^ 𝑁 ) )
36 35 adantr ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ ( 1 ..^ 𝑁 ) )
37 4 36 sselid ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ ℕ )
38 37 nnred ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ ℝ )
39 simpr ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
40 nfcv ⊢ Ⅎ 𝑛 𝑘
41 1 nfcri ⊢ Ⅎ 𝑛 𝑥 ∈ 𝐵
42 2 eleq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
43 40 17 41 42 elrabf ⊢ ( 𝑘 ∈ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ↔ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 ∈ 𝐵 ) )
44 36 39 43 sylanbrc ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } )
45 infssuzle ⊢ ( ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑘 ∈ { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } ) → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ≤ 𝑘 )
46 7 44 45 sylancr ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ≤ 𝑘 )
47 elfzolt2 ⊢ ( 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) → 𝑘 < inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) )
48 47 ad2antlr ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 < inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) )
49 31 38 31 46 48 lelttrd ⊢ ( ( ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) ) ∧ 𝑥 ∈ 𝐵 ) → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) < inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) )
50 49 rexlimdva2 ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ( ∃ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝑥 ∈ 𝐵 → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) < inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) )
51 30 50 syl5bi ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 → inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) < inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) )
52 29 51 mtod ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 )
53 24 52 eldifd ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → 𝑥 ∈ ( ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 ) )
54 csbeq1 ⊢ ( 𝑚 = inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 = ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 )
55 oveq2 ⊢ ( 𝑚 = inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) → ( 1 ..^ 𝑚 ) = ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) )
56 55 iuneq1d ⊢ ( 𝑚 = inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 )
57 54 56 difeq12d ⊢ ( 𝑚 = inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) → ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 ) = ( ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 ) )
58 57 eleq2d ⊢ ( 𝑚 = inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) → ( 𝑥 ∈ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 ) ↔ 𝑥 ∈ ( ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 ) ) )
59 58 rspcev ⊢ ( ( inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ( 1 ..^ 𝑁 ) ∧ 𝑥 ∈ ( ⦋ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ inf ( { 𝑛 ∈ ( 1 ..^ 𝑁 ) ∣ 𝑥 ∈ 𝐴 } , ℝ , < ) ) 𝐵 ) ) → ∃ 𝑚 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 ) )
60 12 53 59 syl2anc ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ∃ 𝑚 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 ) )
61 nfv ⊢ Ⅎ 𝑚 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )
62 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
63 nfcv ⊢ Ⅎ 𝑛 ( 1 ..^ 𝑚 )
64 63 1 nfiun ⊢ Ⅎ 𝑛 ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵
65 62 64 nfdif ⊢ Ⅎ 𝑛 ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 )
66 65 nfcri ⊢ Ⅎ 𝑛 𝑥 ∈ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 )
67 csbeq1a ⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
68 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑚 ) )
69 68 iuneq1d ⊢ ( 𝑛 = 𝑚 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 )
70 67 69 difeq12d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 ) )
71 70 eleq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ↔ 𝑥 ∈ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 ) ) )
72 61 66 71 cbvrexw ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ↔ ∃ 𝑚 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑚 ) 𝐵 ) )
73 60 72 sylibr ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 → ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
74 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) → 𝑥 ∈ 𝐴 )
75 74 reximi ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) → ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 )
76 73 75 impbii ⊢ ( ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 ↔ ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
77 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝐴 ↔ ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ 𝐴 )
78 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ..^ 𝑁 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ↔ ∃ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
79 76 77 78 3bitr4i ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝐴 ↔ 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ..^ 𝑁 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
80 79 eqriv ⊢ ∪ 𝑛 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ∪ 𝑛 ∈ ( 1 ..^ 𝑁 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )