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