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∈AB∈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∈vB=⋃x∈∅B
8 7 eleq1d ⊢v=∅→⋃x∈vB∈D↔⋃x∈∅B∈D
9 6 8 imbi12d ⊢v=∅→v≠∅→⋃x∈vB∈D↔∅≠∅→⋃x∈∅B∈D
10 neeq1 ⊢v=w→v≠∅↔w≠∅
11 iuneq1 ⊢v=w→⋃x∈vB=⋃x∈wB
12 11 eleq1d ⊢v=w→⋃x∈vB∈D↔⋃x∈wB∈D
13 10 12 imbi12d ⊢v=w→v≠∅→⋃x∈vB∈D↔w≠∅→⋃x∈wB∈D
14 neeq1 ⊢v=w∪u→v≠∅↔w∪u≠∅
15 iuneq1 ⊢v=w∪u→⋃x∈vB=⋃x∈w∪uB
16 15 eleq1d ⊢v=w∪u→⋃x∈vB∈D↔⋃x∈w∪uB∈D
17 14 16 imbi12d ⊢v=w∪u→v≠∅→⋃x∈vB∈D↔w∪u≠∅→⋃x∈w∪uB∈D
18 neeq1 ⊢v=A→v≠∅↔A≠∅
19 iuneq1 ⊢v=A→⋃x∈vB=⋃x∈AB
20 19 eleq1d ⊢v=A→⋃x∈vB∈D↔⋃x∈AB∈D
21 18 20 imbi12d ⊢v=A→v≠∅→⋃x∈vB∈D↔A≠∅→⋃x∈AB∈D
22 neirr ⊢¬∅≠∅
23 22 pm2.21i ⊢∅≠∅→⋃x∈∅B∈D
24 23 a1i ⊢φ→∅≠∅→⋃x∈∅B∈D
25 iunxun ⊢⋃x∈w∪uB=⋃x∈wB∪⋃x∈uB
26 nfcsb1v ⊢Ⅎ_x⦋u/x⦌B
27 vex ⊢u∈V
28 csbeq1a ⊢x=u→B=⦋u/x⦌B
29 26 27 28 iunxsnf ⊢⋃x∈uB=⦋u/x⦌B
30 29 uneq2i ⊢⋃x∈wB∪⋃x∈uB=⋃x∈wB∪⦋u/x⦌B
31 25 30 eqtri ⊢⋃x∈w∪uB=⋃x∈wB∪⦋u/x⦌B
32 iuneq1 ⊢w=∅→⋃x∈wB=⋃x∈∅B
33 0iun ⊢⋃x∈∅B=∅
34 33 a1i ⊢w=∅→⋃x∈∅B=∅
35 32 34 eqtrd ⊢w=∅→⋃x∈wB=∅
36 35 uneq1d ⊢w=∅→⋃x∈wB∪⦋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∈wB∪⦋u/x⦌B=⦋u/x⦌B∪⦋u/x⦌B
42 41 adantl ⊢φ∧u∈A∖w∧w=∅→⋃x∈wB∪⦋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 ⊢Ⅎxu∈A
47 1 46 nfan ⊢Ⅎxφ∧u∈A
48 nfcv ⊢Ⅎ_xD
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∈wB∪⦋u/x⦌B∈D
60 59 adantlr ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D∧w=∅→⋃x∈wB∪⦋u/x⦌B∈D
61 simplll ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D∧¬w=∅→φ
62 44 ad3antlr ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D∧¬w=∅→u∈A
63 neqne ⊢¬w=∅→w≠∅
64 63 adantl ⊢w≠∅→⋃x∈wB∈D∧¬w=∅→w≠∅
65 simpl ⊢w≠∅→⋃x∈wB∈D∧¬w=∅→w≠∅→⋃x∈wB∈D
66 64 65 mpd ⊢w≠∅→⋃x∈wB∈D∧¬w=∅→⋃x∈wB∈D
67 66 adantll ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D∧¬w=∅→⋃x∈wB∈D
68 55 3adant3 ⊢φ∧u∈A∧⋃x∈wB∈D→⦋u/x⦌B∈D
69 simp3 ⊢φ∧u∈A∧⋃x∈wB∈D→⋃x∈wB∈D
70 simp1 ⊢φ∧u∈A∧⋃x∈wB∈D→φ
71 70 69 68 3jca ⊢φ∧u∈A∧⋃x∈wB∈D→φ∧⋃x∈wB∈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∈wB∈D∧z∈D↔φ∧⋃x∈wB∈D∧⦋u/x⦌B∈D
74 uneq2 ⊢z=⦋u/x⦌B→⋃x∈wB∪z=⋃x∈wB∪⦋u/x⦌B
75 74 eleq1d ⊢z=⦋u/x⦌B→⋃x∈wB∪z∈D↔⋃x∈wB∪⦋u/x⦌B∈D
76 73 75 imbi12d ⊢z=⦋u/x⦌B→φ∧⋃x∈wB∈D∧z∈D→⋃x∈wB∪z∈D↔φ∧⋃x∈wB∈D∧⦋u/x⦌B∈D→⋃x∈wB∪⦋u/x⦌B∈D
77 76 imbi2d ⊢z=⦋u/x⦌B→⋃x∈wB∈D→φ∧⋃x∈wB∈D∧z∈D→⋃x∈wB∪z∈D↔⋃x∈wB∈D→φ∧⋃x∈wB∈D∧⦋u/x⦌B∈D→⋃x∈wB∪⦋u/x⦌B∈D
78 eleq1 ⊢y=⋃x∈wB→y∈D↔⋃x∈wB∈D
79 78 3anbi2d ⊢y=⋃x∈wB→φ∧y∈D∧z∈D↔φ∧⋃x∈wB∈D∧z∈D
80 uneq1 ⊢y=⋃x∈wB→y∪z=⋃x∈wB∪z
81 80 eleq1d ⊢y=⋃x∈wB→y∪z∈D↔⋃x∈wB∪z∈D
82 79 81 imbi12d ⊢y=⋃x∈wB→φ∧y∈D∧z∈D→y∪z∈D↔φ∧⋃x∈wB∈D∧z∈D→⋃x∈wB∪z∈D
83 82 3 vtoclg ⊢⋃x∈wB∈D→φ∧⋃x∈wB∈D∧z∈D→⋃x∈wB∪z∈D
84 77 83 vtoclg ⊢⦋u/x⦌B∈D→⋃x∈wB∈D→φ∧⋃x∈wB∈D∧⦋u/x⦌B∈D→⋃x∈wB∪⦋u/x⦌B∈D
85 68 69 71 84 syl3c ⊢φ∧u∈A∧⋃x∈wB∈D→⋃x∈wB∪⦋u/x⦌B∈D
86 61 62 67 85 syl3anc ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D∧¬w=∅→⋃x∈wB∪⦋u/x⦌B∈D
87 60 86 pm2.61dan ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D→⋃x∈wB∪⦋u/x⦌B∈D
88 31 87 eqeltrid ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D→⋃x∈w∪uB∈D
89 88 a1d ⊢φ∧u∈A∖w∧w≠∅→⋃x∈wB∈D→w∪u≠∅→⋃x∈w∪uB∈D
90 89 ex ⊢φ∧u∈A∖w→w≠∅→⋃x∈wB∈D→w∪u≠∅→⋃x∈w∪uB∈D
91 90 adantrl ⊢φ∧w⊆A∧u∈A∖w→w≠∅→⋃x∈wB∈D→w∪u≠∅→⋃x∈w∪uB∈D
92 9 13 17 21 24 91 4 findcard2d ⊢φ→A≠∅→⋃x∈AB∈D
93 5 92 mpd ⊢φ→⋃x∈AB∈D