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 bilani 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> ( U. J u. U. B ) = U. J )
5 eqid 
 |-  U. J = U. J
6 eqid 
 |-  U. A = U. A
7 5 6 locfinbas 
 |-  ( A e. ( LocFin ` J ) -> U. J = U. A )
8 7 ad2antrr 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> U. J = U. A )
9 8 uneq1d 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> ( U. J u. U. B ) = ( U. A u. U. B ) )
10 4 9 eqtr3d 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> U. J = ( U. A u. U. B ) )
11 uniun 
 |-  U. ( A u. B ) = ( U. A u. U. B )
12 10 11 eqtr4di 
 |-  ( ( ( A e. ( LocFin ` J ) /\ B e. Fin ) /\ U. B C_ U. J ) -> U. J = U. ( A u. B ) )
13 5 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 ) )
14 13 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 ) )
15 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 )
16 rabfi 
 |-  ( B e. Fin -> { s e. B | ( s i^i n ) =/= (/) } e. Fin )
17 16 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 )
18 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 ) =/= (/) } )
19 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 )
20 18 19 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 )
21 15 17 20 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 )
22 21 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 ) )
23 22 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 ) )
24 23 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 ) ) )
25 24 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 ) ) )
26 14 25 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 ) )
27 26 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 ) )
28 2 12 27 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 ) ) )
29 28 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 ) ) )
30 eqid 
 |-  U. ( A u. B ) = U. ( A u. B )
31 5 30 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 ) ) )
32 29 31 sylibr 
 |-  ( ( A e. ( LocFin ` J ) /\ B e. Fin /\ U. B C_ U. J ) -> ( A u. B ) e. ( LocFin ` J ) )