Metamath Proof Explorer

Theorem fiiuncl

Description: If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fiiuncl.xph ⊢ Ⅎ x φ
fiiuncl.b ⊢ φ ∧ x ∈ A → B ∈ D
fiiuncl.un ⊢ φ ∧ y ∈ D ∧ z ∈ D → y ∪ z ∈ D
fiiuncl.a ⊢ φ → A ∈ Fin
fiiuncl.n0 ⊢ φ → A ≠ ∅
Assertion fiiuncl ⊢ φ → ⋃ x ∈ A B ∈ D

Proof

Step Hyp Ref Expression
1 fiiuncl.xph ⊢ Ⅎ x φ
2 fiiuncl.b ⊢ φ ∧ x ∈ A → B ∈ D
3 fiiuncl.un ⊢ φ ∧ y ∈ D ∧ z ∈ D → y ∪ z ∈ D
4 fiiuncl.a ⊢ φ → A ∈ Fin
5 fiiuncl.n0 ⊢ φ → A ≠ ∅
6 neeq1 ⊢ v = ∅ → v ≠ ∅ ↔ ∅ ≠ ∅
7 iuneq1 ⊢ v = ∅ → ⋃ x ∈ v B = ⋃ x ∈ ∅ B
8 7 eleq1d ⊢ v = ∅ → ⋃ x ∈ v B ∈ D ↔ ⋃ x ∈ ∅ B ∈ D
9 6 8 imbi12d ⊢ v = ∅ → v ≠ ∅ → ⋃ x ∈ v B ∈ D ↔ ∅ ≠ ∅ → ⋃ x ∈ ∅ B ∈ D
10 neeq1 ⊢ v = w → v ≠ ∅ ↔ w ≠ ∅
11 iuneq1 ⊢ v = w → ⋃ x ∈ v B = ⋃ x ∈ w B
12 11 eleq1d ⊢ v = w → ⋃ x ∈ v B ∈ D ↔ ⋃ x ∈ w B ∈ D
13 10 12 imbi12d ⊢ v = w → v ≠ ∅ → ⋃ x ∈ v B ∈ D ↔ w ≠ ∅ → ⋃ x ∈ w B ∈ D
14 neeq1 ⊢ v = w ∪ u → v ≠ ∅ ↔ w ∪ u ≠ ∅
15 iuneq1 ⊢ v = w ∪ u → ⋃ x ∈ v B = ⋃ x ∈ w ∪ u B
16 15 eleq1d ⊢ v = w ∪ u → ⋃ x ∈ v B ∈ D ↔ ⋃ x ∈ w ∪ u B ∈ D
17 14 16 imbi12d ⊢ v = w ∪ u → v ≠ ∅ → ⋃ x ∈ v B ∈ D ↔ w ∪ u ≠ ∅ → ⋃ x ∈ w ∪ u B ∈ D
18 neeq1 ⊢ v = A → v ≠ ∅ ↔ A ≠ ∅
19 iuneq1 ⊢ v = A → ⋃ x ∈ v B = ⋃ x ∈ A B
20 19 eleq1d ⊢ v = A → ⋃ x ∈ v B ∈ D ↔ ⋃ x ∈ A B ∈ D
21 18 20 imbi12d ⊢ v = A → v ≠ ∅ → ⋃ x ∈ v B ∈ D ↔ A ≠ ∅ → ⋃ x ∈ A B ∈ D
22 neirr ⊢ ¬ ∅ ≠ ∅
23 22 pm2.21i ⊢ ∅ ≠ ∅ → ⋃ x ∈ ∅ B ∈ D
24 23 a1i ⊢ φ → ∅ ≠ ∅ → ⋃ x ∈ ∅ B ∈ D
25 iunxun ⊢ ⋃ x ∈ w ∪ u B = ⋃ x ∈ w B ∪ ⋃ x ∈ u B
26 nfcsb1v ⊢ Ⅎ _ x ⦋ u / x⦌ B
27 vex ⊢ u ∈ V
28 csbeq1a ⊢ x = u → B = ⦋ u / x⦌ B
29 26 27 28 iunxsnf ⊢ ⋃ x ∈ u B = ⦋ u / x⦌ B
30 29 uneq2i ⊢ ⋃ x ∈ w B ∪ ⋃ x ∈ u B = ⋃ x ∈ w B ∪ ⦋ u / x⦌ B
31 25 30 eqtri ⊢ ⋃ x ∈ w ∪ u B = ⋃ x ∈ w B ∪ ⦋ u / x⦌ B
32 iuneq1 ⊢ w = ∅ → ⋃ x ∈ w B = ⋃ x ∈ ∅ B
33 0iun ⊢ ⋃ x ∈ ∅ B = ∅
34 33 a1i ⊢ w = ∅ → ⋃ x ∈ ∅ B = ∅
35 32 34 eqtrd ⊢ w = ∅ → ⋃ x ∈ w B = ∅
36 35 uneq1d ⊢ w = ∅ → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B = ∅ ∪ ⦋ u / x⦌ B
37 0un ⊢ ∅ ∪ ⦋ u / x⦌ B = ⦋ u / x⦌ B
38 unidm ⊢ ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B = ⦋ u / x⦌ B
39 37 38 eqtr4i ⊢ ∅ ∪ ⦋ u / x⦌ B = ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B
40 39 a1i ⊢ w = ∅ → ∅ ∪ ⦋ u / x⦌ B = ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B
41 36 40 eqtrd ⊢ w = ∅ → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B = ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B
42 41 adantl ⊢ φ ∧ u ∈ A ∖ w ∧ w = ∅ → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B = ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B
43 simpl ⊢ φ ∧ u ∈ A ∖ w → φ
44 eldifi ⊢ u ∈ A ∖ w → u ∈ A
45 44 adantl ⊢ φ ∧ u ∈ A ∖ w → u ∈ A
46 nfv ⊢ Ⅎ x u ∈ A
47 1 46 nfan ⊢ Ⅎ x φ ∧ u ∈ A
48 nfcv ⊢ Ⅎ _ x D
49 26 48 nfel ⊢ Ⅎ x ⦋ u / x⦌ B ∈ D
50 47 49 nfim ⊢ Ⅎ x φ ∧ u ∈ A → ⦋ u / x⦌ B ∈ D
51 eleq1 ⊢ x = u → x ∈ A ↔ u ∈ A
52 51 anbi2d ⊢ x = u → φ ∧ x ∈ A ↔ φ ∧ u ∈ A
53 28 eleq1d ⊢ x = u → B ∈ D ↔ ⦋ u / x⦌ B ∈ D
54 52 53 imbi12d ⊢ x = u → φ ∧ x ∈ A → B ∈ D ↔ φ ∧ u ∈ A → ⦋ u / x⦌ B ∈ D
55 50 54 2 chvarfv ⊢ φ ∧ u ∈ A → ⦋ u / x⦌ B ∈ D
56 38 55 eqeltrid ⊢ φ ∧ u ∈ A → ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B ∈ D
57 43 45 56 syl2anc ⊢ φ ∧ u ∈ A ∖ w → ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B ∈ D
58 57 adantr ⊢ φ ∧ u ∈ A ∖ w ∧ w = ∅ → ⦋ u / x⦌ B ∪ ⦋ u / x⦌ B ∈ D
59 42 58 eqeltrd ⊢ φ ∧ u ∈ A ∖ w ∧ w = ∅ → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
60 59 adantlr ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ w = ∅ → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
61 simplll ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ ¬ w = ∅ → φ
62 44 ad3antlr ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ ¬ w = ∅ → u ∈ A
63 neqne ⊢ ¬ w = ∅ → w ≠ ∅
64 63 adantl ⊢ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ ¬ w = ∅ → w ≠ ∅
65 simpl ⊢ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ ¬ w = ∅ → w ≠ ∅ → ⋃ x ∈ w B ∈ D
66 64 65 mpd ⊢ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ ¬ w = ∅ → ⋃ x ∈ w B ∈ D
67 66 adantll ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ ¬ w = ∅ → ⋃ x ∈ w B ∈ D
68 55 3adant3 ⊢ φ ∧ u ∈ A ∧ ⋃ x ∈ w B ∈ D → ⦋ u / x⦌ B ∈ D
69 simp3 ⊢ φ ∧ u ∈ A ∧ ⋃ x ∈ w B ∈ D → ⋃ x ∈ w B ∈ D
70 simp1 ⊢ φ ∧ u ∈ A ∧ ⋃ x ∈ w B ∈ D → φ
71 70 69 68 3jca ⊢ φ ∧ u ∈ A ∧ ⋃ x ∈ w B ∈ D → φ ∧ ⋃ x ∈ w B ∈ D ∧ ⦋ u / x⦌ B ∈ D
72 eleq1 ⊢ z = ⦋ u / x⦌ B → z ∈ D ↔ ⦋ u / x⦌ B ∈ D
73 72 3anbi3d ⊢ z = ⦋ u / x⦌ B → φ ∧ ⋃ x ∈ w B ∈ D ∧ z ∈ D ↔ φ ∧ ⋃ x ∈ w B ∈ D ∧ ⦋ u / x⦌ B ∈ D
74 uneq2 ⊢ z = ⦋ u / x⦌ B → ⋃ x ∈ w B ∪ z = ⋃ x ∈ w B ∪ ⦋ u / x⦌ B
75 74 eleq1d ⊢ z = ⦋ u / x⦌ B → ⋃ x ∈ w B ∪ z ∈ D ↔ ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
76 73 75 imbi12d ⊢ z = ⦋ u / x⦌ B → φ ∧ ⋃ x ∈ w B ∈ D ∧ z ∈ D → ⋃ x ∈ w B ∪ z ∈ D ↔ φ ∧ ⋃ x ∈ w B ∈ D ∧ ⦋ u / x⦌ B ∈ D → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
77 76 imbi2d ⊢ z = ⦋ u / x⦌ B → ⋃ x ∈ w B ∈ D → φ ∧ ⋃ x ∈ w B ∈ D ∧ z ∈ D → ⋃ x ∈ w B ∪ z ∈ D ↔ ⋃ x ∈ w B ∈ D → φ ∧ ⋃ x ∈ w B ∈ D ∧ ⦋ u / x⦌ B ∈ D → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
78 eleq1 ⊢ y = ⋃ x ∈ w B → y ∈ D ↔ ⋃ x ∈ w B ∈ D
79 78 3anbi2d ⊢ y = ⋃ x ∈ w B → φ ∧ y ∈ D ∧ z ∈ D ↔ φ ∧ ⋃ x ∈ w B ∈ D ∧ z ∈ D
80 uneq1 ⊢ y = ⋃ x ∈ w B → y ∪ z = ⋃ x ∈ w B ∪ z
81 80 eleq1d ⊢ y = ⋃ x ∈ w B → y ∪ z ∈ D ↔ ⋃ x ∈ w B ∪ z ∈ D
82 79 81 imbi12d ⊢ y = ⋃ x ∈ w B → φ ∧ y ∈ D ∧ z ∈ D → y ∪ z ∈ D ↔ φ ∧ ⋃ x ∈ w B ∈ D ∧ z ∈ D → ⋃ x ∈ w B ∪ z ∈ D
83 82 3 vtoclg ⊢ ⋃ x ∈ w B ∈ D → φ ∧ ⋃ x ∈ w B ∈ D ∧ z ∈ D → ⋃ x ∈ w B ∪ z ∈ D
84 77 83 vtoclg ⊢ ⦋ u / x⦌ B ∈ D → ⋃ x ∈ w B ∈ D → φ ∧ ⋃ x ∈ w B ∈ D ∧ ⦋ u / x⦌ B ∈ D → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
85 68 69 71 84 syl3c ⊢ φ ∧ u ∈ A ∧ ⋃ x ∈ w B ∈ D → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
86 61 62 67 85 syl3anc ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D ∧ ¬ w = ∅ → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
87 60 86 pm2.61dan ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D → ⋃ x ∈ w B ∪ ⦋ u / x⦌ B ∈ D
88 31 87 eqeltrid ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D → ⋃ x ∈ w ∪ u B ∈ D
89 88 a1d ⊢ φ ∧ u ∈ A ∖ w ∧ w ≠ ∅ → ⋃ x ∈ w B ∈ D → w ∪ u ≠ ∅ → ⋃ x ∈ w ∪ u B ∈ D
90 89 ex ⊢ φ ∧ u ∈ A ∖ w → w ≠ ∅ → ⋃ x ∈ w B ∈ D → w ∪ u ≠ ∅ → ⋃ x ∈ w ∪ u B ∈ D
91 90 adantrl ⊢ φ ∧ w ⊆ A ∧ u ∈ A ∖ w → w ≠ ∅ → ⋃ x ∈ w B ∈ D → w ∪ u ≠ ∅ → ⋃ x ∈ w ∪ u B ∈ D
92 9 13 17 21 24 91 4 findcard2d ⊢ φ → A ≠ ∅ → ⋃ x ∈ A B ∈ D
93 5 92 mpd ⊢ φ → ⋃ x ∈ A B ∈ D