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
|- F/ x ph
fiiuncl.b
|- ( ( ph /\ x e. A ) -> B e. D )
fiiuncl.un
|- ( ( ph /\ y e. D /\ z e. D ) -> ( y u. z ) e. D )
fiiuncl.a
|- ( ph -> A e. Fin )
fiiuncl.n0
|- ( ph -> A =/= (/) )
Assertion fiiuncl
|- ( ph -> U_ x e. A B e. D )

Proof

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