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 ⊢Ⅎ_kA
iundisjf.2 ⊢Ⅎ_nB
iundisjf.3 ⊢n=k→A=B
Assertion iundisjf ⊢⋃n∈ℕA=⋃n∈ℕA∖⋃k∈1..^nB

Proof

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