Metamath Proof Explorer

Theorem iundisjf

Description: Rewrite a countable union as a disjoint union. Cf. iundisj . (Contributed by Thierry Arnoux, 31-Dec-2016)

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

Proof

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