Metamath Proof Explorer

Theorem iundisj

Description: Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014)

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

Proof

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