Metamath Proof Explorer

Theorem heiborlem1

Description: Lemma for heibor . We work with a fixed open cover U throughout. The set K is the set of all subsets of X that admit no finite subcover of U . (We wish to prove that K is empty.) If a set C has no finite subcover, then any finite cover of C must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014)

Ref Expression
Hypotheses heibor.1 
|- J = ( MetOpen ` D )
heibor.3 
|- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
heiborlem1.4 
|- B e. _V
Assertion heiborlem1 
|- ( ( A e. Fin /\ C C_ U_ x e. A B /\ C e. K ) -> E. x e. A B e. K )

Proof

Step Hyp Ref Expression
1 heibor.1 
 |-  J = ( MetOpen ` D )
2 heibor.3 
 |-  K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
3 heiborlem1.4 
 |-  B e. _V
4 sseq1 
 |-  ( u = B -> ( u C_ U. v <-> B C_ U. v ) )
5 4 rexbidv 
 |-  ( u = B -> ( E. v e. ( ~P U i^i Fin ) u C_ U. v <-> E. v e. ( ~P U i^i Fin ) B C_ U. v ) )
6 5 notbid 
 |-  ( u = B -> ( -. E. v e. ( ~P U i^i Fin ) u C_ U. v <-> -. E. v e. ( ~P U i^i Fin ) B C_ U. v ) )
7 3 6 2 elab2 
 |-  ( B e. K <-> -. E. v e. ( ~P U i^i Fin ) B C_ U. v )
8 7 con2bii 
 |-  ( E. v e. ( ~P U i^i Fin ) B C_ U. v <-> -. B e. K )
9 8 ralbii 
 |-  ( A. x e. A E. v e. ( ~P U i^i Fin ) B C_ U. v <-> A. x e. A -. B e. K )
10 ralnex 
 |-  ( A. x e. A -. B e. K <-> -. E. x e. A B e. K )
11 9 10 bitr2i 
 |-  ( -. E. x e. A B e. K <-> A. x e. A E. v e. ( ~P U i^i Fin ) B C_ U. v )
12 unieq 
 |-  ( v = ( t ` x ) -> U. v = U. ( t ` x ) )
13 12 sseq2d 
 |-  ( v = ( t ` x ) -> ( B C_ U. v <-> B C_ U. ( t ` x ) ) )
14 13 ac6sfi 
 |-  ( ( A e. Fin /\ A. x e. A E. v e. ( ~P U i^i Fin ) B C_ U. v ) -> E. t ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) )
15 14 ex 
 |-  ( A e. Fin -> ( A. x e. A E. v e. ( ~P U i^i Fin ) B C_ U. v -> E. t ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) )
16 15 adantr 
 |-  ( ( A e. Fin /\ C C_ U_ x e. A B ) -> ( A. x e. A E. v e. ( ~P U i^i Fin ) B C_ U. v -> E. t ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) )
17 sseq1 
 |-  ( u = C -> ( u C_ U. v <-> C C_ U. v ) )
18 17 rexbidv 
 |-  ( u = C -> ( E. v e. ( ~P U i^i Fin ) u C_ U. v <-> E. v e. ( ~P U i^i Fin ) C C_ U. v ) )
19 18 notbid 
 |-  ( u = C -> ( -. E. v e. ( ~P U i^i Fin ) u C_ U. v <-> -. E. v e. ( ~P U i^i Fin ) C C_ U. v ) )
20 19 2 elab2g 
 |-  ( C e. K -> ( C e. K <-> -. E. v e. ( ~P U i^i Fin ) C C_ U. v ) )
21 20 ibi 
 |-  ( C e. K -> -. E. v e. ( ~P U i^i Fin ) C C_ U. v )
22 frn 
 |-  ( t : A --> ( ~P U i^i Fin ) -> ran t C_ ( ~P U i^i Fin ) )
23 22 ad2antrl 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> ran t C_ ( ~P U i^i Fin ) )
24 inss1 
 |-  ( ~P U i^i Fin ) C_ ~P U
25 23 24 sstrdi 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> ran t C_ ~P U )
26 sspwuni 
 |-  ( ran t C_ ~P U <-> U. ran t C_ U )
27 25 26 sylib 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> U. ran t C_ U )
28 vex 
 |-  t e. _V
29 28 rnex 
 |-  ran t e. _V
30 29 uniex 
 |-  U. ran t e. _V
31 30 elpw 
 |-  ( U. ran t e. ~P U <-> U. ran t C_ U )
32 27 31 sylibr 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> U. ran t e. ~P U )
33 ffn 
 |-  ( t : A --> ( ~P U i^i Fin ) -> t Fn A )
34 33 ad2antrl 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> t Fn A )
35 dffn4 
 |-  ( t Fn A <-> t : A -onto-> ran t )
36 34 35 sylib 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> t : A -onto-> ran t )
37 fofi 
 |-  ( ( A e. Fin /\ t : A -onto-> ran t ) -> ran t e. Fin )
38 36 37 syldan 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> ran t e. Fin )
39 inss2 
 |-  ( ~P U i^i Fin ) C_ Fin
40 23 39 sstrdi 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> ran t C_ Fin )
41 unifi 
 |-  ( ( ran t e. Fin /\ ran t C_ Fin ) -> U. ran t e. Fin )
42 38 40 41 syl2anc 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> U. ran t e. Fin )
43 32 42 elind 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> U. ran t e. ( ~P U i^i Fin ) )
44 43 adantlr 
 |-  ( ( ( A e. Fin /\ C C_ U_ x e. A B ) /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> U. ran t e. ( ~P U i^i Fin ) )
45 simplr 
 |-  ( ( ( A e. Fin /\ C C_ U_ x e. A B ) /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> C C_ U_ x e. A B )
46 fnfvelrn 
 |-  ( ( t Fn A /\ x e. A ) -> ( t ` x ) e. ran t )
47 33 46 sylan 
 |-  ( ( t : A --> ( ~P U i^i Fin ) /\ x e. A ) -> ( t ` x ) e. ran t )
48 47 adantll 
 |-  ( ( ( A e. Fin /\ t : A --> ( ~P U i^i Fin ) ) /\ x e. A ) -> ( t ` x ) e. ran t )
49 elssuni 
 |-  ( ( t ` x ) e. ran t -> ( t ` x ) C_ U. ran t )
50 uniss 
 |-  ( ( t ` x ) C_ U. ran t -> U. ( t ` x ) C_ U. U. ran t )
51 48 49 50 3syl 
 |-  ( ( ( A e. Fin /\ t : A --> ( ~P U i^i Fin ) ) /\ x e. A ) -> U. ( t ` x ) C_ U. U. ran t )
52 sstr2 
 |-  ( B C_ U. ( t ` x ) -> ( U. ( t ` x ) C_ U. U. ran t -> B C_ U. U. ran t ) )
53 51 52 syl5com 
 |-  ( ( ( A e. Fin /\ t : A --> ( ~P U i^i Fin ) ) /\ x e. A ) -> ( B C_ U. ( t ` x ) -> B C_ U. U. ran t ) )
54 53 ralimdva 
 |-  ( ( A e. Fin /\ t : A --> ( ~P U i^i Fin ) ) -> ( A. x e. A B C_ U. ( t ` x ) -> A. x e. A B C_ U. U. ran t ) )
55 54 impr 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> A. x e. A B C_ U. U. ran t )
56 iunss 
 |-  ( U_ x e. A B C_ U. U. ran t <-> A. x e. A B C_ U. U. ran t )
57 55 56 sylibr 
 |-  ( ( A e. Fin /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> U_ x e. A B C_ U. U. ran t )
58 57 adantlr 
 |-  ( ( ( A e. Fin /\ C C_ U_ x e. A B ) /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> U_ x e. A B C_ U. U. ran t )
59 45 58 sstrd 
 |-  ( ( ( A e. Fin /\ C C_ U_ x e. A B ) /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> C C_ U. U. ran t )
60 unieq 
 |-  ( v = U. ran t -> U. v = U. U. ran t )
61 60 sseq2d 
 |-  ( v = U. ran t -> ( C C_ U. v <-> C C_ U. U. ran t ) )
62 61 rspcev 
 |-  ( ( U. ran t e. ( ~P U i^i Fin ) /\ C C_ U. U. ran t ) -> E. v e. ( ~P U i^i Fin ) C C_ U. v )
63 44 59 62 syl2anc 
 |-  ( ( ( A e. Fin /\ C C_ U_ x e. A B ) /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> E. v e. ( ~P U i^i Fin ) C C_ U. v )
64 21 63 nsyl3 
 |-  ( ( ( A e. Fin /\ C C_ U_ x e. A B ) /\ ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) ) -> -. C e. K )
65 64 ex 
 |-  ( ( A e. Fin /\ C C_ U_ x e. A B ) -> ( ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) -> -. C e. K ) )
66 65 exlimdv 
 |-  ( ( A e. Fin /\ C C_ U_ x e. A B ) -> ( E. t ( t : A --> ( ~P U i^i Fin ) /\ A. x e. A B C_ U. ( t ` x ) ) -> -. C e. K ) )
67 16 66 syld 
 |-  ( ( A e. Fin /\ C C_ U_ x e. A B ) -> ( A. x e. A E. v e. ( ~P U i^i Fin ) B C_ U. v -> -. C e. K ) )
68 11 67 syl5bi 
 |-  ( ( A e. Fin /\ C C_ U_ x e. A B ) -> ( -. E. x e. A B e. K -> -. C e. K ) )
69 68 con4d 
 |-  ( ( A e. Fin /\ C C_ U_ x e. A B ) -> ( C e. K -> E. x e. A B e. K ) )
70 69 3impia 
 |-  ( ( A e. Fin /\ C C_ U_ x e. A B /\ C e. K ) -> E. x e. A B e. K )