Metamath Proof Explorer

Theorem lfinun

Description: Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020)

Ref Expression
Assertion lfinun 
|- ( ( A e. ( LocFin ` J ) /\ B e. Fin /\ U. B C_ U. J ) -> ( A u. B ) e. ( LocFin ` J ) )

Proof

Step Hyp Ref Expression
1 locfintop 
 |-  ( A e. ( LocFin ` J ) -> J e. Top )
2 1 ad2antrr 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> J e. Top )
3 ssequn2 
 |-  ( U. B C_ U. J <-> ( U. J u. U. B ) = U. J )
4 3 biimpi 
 |-  ( U. B C_ U. J -> ( U. J u. U. B ) = U. J )
5 4 adantl 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> ( U. J u. U. B ) = U. J )
6 eqid 
 |-  U. J = U. J
7 eqid 
 |-  U. A = U. A
8 6 7 locfinbas 
 |-  ( A e. ( LocFin ` J ) -> U. J = U. A )
9 8 ad2antrr 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> U. J = U. A )
10 9 uneq1d 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> ( U. J u. U. B ) = ( U. A u. U. B ) )
11 5 10 eqtr3d 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> U. J = ( U. A u. U. B ) )
12 uniun 
 |-  U. ( A u. B ) = ( U. A u. U. B )
13 11 12 eqtr4di 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> U. J = U. ( A u. B ) )
14 6 locfinnei 
 |-  ( ( A e. ( LocFin ` J ) /\ x e. U. J ) -> E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
15 14 ad4ant14 
 |-  ( ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) /\ x e. U. J ) -> E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
16 simpr 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) -> { s e. A | ( s i^i n ) =/= (/) } e. Fin )
17 rabfi 
 |-  ( B e. Fin -> { s e. B | ( s i^i n ) =/= (/) } e. Fin )
18 17 ad2antlr 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) -> { s e. B | ( s i^i n ) =/= (/) } e. Fin )
19 rabun2 
 |-  { s e. ( A u. B ) | ( s i^i n ) =/= (/) } = ( { s e. A | ( s i^i n ) =/= (/) } u. { s e. B | ( s i^i n ) =/= (/) } )
20 unfi 
 |-  ( ( { s e. A | ( s i^i n ) =/= (/) } e. Fin /\ { s e. B | ( s i^i n ) =/= (/) } e. Fin ) -> ( { s e. A | ( s i^i n ) =/= (/) } u. { s e. B | ( s i^i n ) =/= (/) } ) e. Fin )
21 19 20 eqeltrid 
 |-  ( ( { s e. A | ( s i^i n ) =/= (/) } e. Fin /\ { s e. B | ( s i^i n ) =/= (/) } e. Fin ) -> { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin )
22 16 18 21 syl2anc 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) -> { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin )
23 22 ex 
 |-  ( ( A e. ( LocFin ` J ) /\ B e. Fin ) -> ( { s e. A | ( s i^i n ) =/= (/) } e. Fin -> { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) )
24 23 ad2antrr 
 |-  ( ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) /\ x e. U. J ) -> ( { s e. A | ( s i^i n ) =/= (/) } e. Fin -> { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) )
25 24 anim2d 
 |-  ( ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) /\ x e. U. J ) -> ( ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) -> ( x e. n /\ { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) ) )
26 25 reximdv 
 |-  ( ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) /\ x e. U. J ) -> ( E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) -> E. n e. J ( x e. n /\ { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) ) )
27 15 26 mpd 
 |-  ( ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) /\ x e. U. J ) -> E. n e. J ( x e. n /\ { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) )
28 27 ralrimiva 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> A. x e. U. J E. n e. J ( x e. n /\ { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) )
29 2 13 28 3jca 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> ( J e. Top /\ U. J = U. ( A u. B ) /\ A. x e. U. J E. n e. J ( x e. n /\ { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) ) )
30 29 3impa 
 |-  ( ( A e. ( LocFin ` J ) /\ B e. Fin /\ U. B C_ U. J ) -> ( J e. Top /\ U. J = U. ( A u. B ) /\ A. x e. U. J E. n e. J ( x e. n /\ { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) ) )
31 eqid 
 |-  U. ( A u. B ) = U. ( A u. B )
32 6 31 islocfin 
 |-  ( ( A u. B ) e. ( LocFin ` J ) <-> ( J e. Top /\ U. J = U. ( A u. B ) /\ A. x e. U. J E. n e. J ( x e. n /\ { s e. ( A u. B ) | ( s i^i n ) =/= (/) } e. Fin ) ) )
33 30 32 sylibr 
 |-  ( ( A e. ( LocFin ` J ) /\ B e. Fin /\ U. B C_ U. J ) -> ( A u. B ) e. ( LocFin ` J ) )