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 )