This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
heiborlem1.4 ⊢ 𝐵 ∈ V
Assertion heiborlem1 ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3 heiborlem1.4 ⊢ 𝐵 ∈ V
4 sseq1 ⊢ ( 𝑢 = 𝐵 → ( 𝑢 ⊆ ∪ 𝑣 ↔ 𝐵 ⊆ ∪ 𝑣 ) )
5 4 rexbidv ⊢ ( 𝑢 = 𝐵 → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 ) )
6 5 notbid ⊢ ( 𝑢 = 𝐵 → ( ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 ) )
7 3 6 2 elab2 ⊢ ( 𝐵 ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 )
8 7 con2bii ⊢ ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 ↔ ¬ 𝐵 ∈ 𝐾 )
9 8 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 ∈ 𝐾 )
10 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 ∈ 𝐾 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 )
11 9 10 bitr2i ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 )
12 unieq ⊢ ( 𝑣 = ( 𝑡 ‘ 𝑥 ) → ∪ 𝑣 = ∪ ( 𝑡 ‘ 𝑥 ) )
13 12 sseq2d ⊢ ( 𝑣 = ( 𝑡 ‘ 𝑥 ) → ( 𝐵 ⊆ ∪ 𝑣 ↔ 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) )
14 13 ac6sfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 ) → ∃ 𝑡 ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) )
15 14 ex ⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 → ∃ 𝑡 ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) )
16 15 adantr ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 → ∃ 𝑡 ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) )
17 sseq1 ⊢ ( 𝑢 = 𝐶 → ( 𝑢 ⊆ ∪ 𝑣 ↔ 𝐶 ⊆ ∪ 𝑣 ) )
18 17 rexbidv ⊢ ( 𝑢 = 𝐶 → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐶 ⊆ ∪ 𝑣 ) )
19 18 notbid ⊢ ( 𝑢 = 𝐶 → ( ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐶 ⊆ ∪ 𝑣 ) )
20 19 2 elab2g ⊢ ( 𝐶 ∈ 𝐾 → ( 𝐶 ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐶 ⊆ ∪ 𝑣 ) )
21 20 ibi ⊢ ( 𝐶 ∈ 𝐾 → ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐶 ⊆ ∪ 𝑣 )
22 frn ⊢ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) → ran 𝑡 ⊆ ( 𝒫 𝑈 ∩ Fin ) )
23 22 ad2antrl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ran 𝑡 ⊆ ( 𝒫 𝑈 ∩ Fin ) )
24 inss1 ⊢ ( 𝒫 𝑈 ∩ Fin ) ⊆ 𝒫 𝑈
25 23 24 sstrdi ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ran 𝑡 ⊆ 𝒫 𝑈 )
26 sspwuni ⊢ ( ran 𝑡 ⊆ 𝒫 𝑈 ↔ ∪ ran 𝑡 ⊆ 𝑈 )
27 25 26 sylib ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∪ ran 𝑡 ⊆ 𝑈 )
28 vex ⊢ 𝑡 ∈ V
29 28 rnex ⊢ ran 𝑡 ∈ V
30 29 uniex ⊢ ∪ ran 𝑡 ∈ V
31 30 elpw ⊢ ( ∪ ran 𝑡 ∈ 𝒫 𝑈 ↔ ∪ ran 𝑡 ⊆ 𝑈 )
32 27 31 sylibr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∪ ran 𝑡 ∈ 𝒫 𝑈 )
33 ffn ⊢ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) → 𝑡 Fn 𝐴 )
34 33 ad2antrl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → 𝑡 Fn 𝐴 )
35 dffn4 ⊢ ( 𝑡 Fn 𝐴 ↔ 𝑡 : 𝐴 –onto→ ran 𝑡 )
36 34 35 sylib ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → 𝑡 : 𝐴 –onto→ ran 𝑡 )
37 fofi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑡 : 𝐴 –onto→ ran 𝑡 ) → ran 𝑡 ∈ Fin )
38 36 37 syldan ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ran 𝑡 ∈ Fin )
39 inss2 ⊢ ( 𝒫 𝑈 ∩ Fin ) ⊆ Fin
40 23 39 sstrdi ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ran 𝑡 ⊆ Fin )
41 unifi ⊢ ( ( ran 𝑡 ∈ Fin ∧ ran 𝑡 ⊆ Fin ) → ∪ ran 𝑡 ∈ Fin )
42 38 40 41 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∪ ran 𝑡 ∈ Fin )
43 32 42 elind ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∪ ran 𝑡 ∈ ( 𝒫 𝑈 ∩ Fin ) )
44 43 adantlr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∪ ran 𝑡 ∈ ( 𝒫 𝑈 ∩ Fin ) )
45 simplr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
46 fnfvelrn ⊢ ( ( 𝑡 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑡 ‘ 𝑥 ) ∈ ran 𝑡 )
47 33 46 sylan ⊢ ( ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑡 ‘ 𝑥 ) ∈ ran 𝑡 )
48 47 adantll ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑡 ‘ 𝑥 ) ∈ ran 𝑡 )
49 elssuni ⊢ ( ( 𝑡 ‘ 𝑥 ) ∈ ran 𝑡 → ( 𝑡 ‘ 𝑥 ) ⊆ ∪ ran 𝑡 )
50 uniss ⊢ ( ( 𝑡 ‘ 𝑥 ) ⊆ ∪ ran 𝑡 → ∪ ( 𝑡 ‘ 𝑥 ) ⊆ ∪ ∪ ran 𝑡 )
51 48 49 50 3syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ∪ ( 𝑡 ‘ 𝑥 ) ⊆ ∪ ∪ ran 𝑡 )
52 sstr2 ⊢ ( 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) → ( ∪ ( 𝑡 ‘ 𝑥 ) ⊆ ∪ ∪ ran 𝑡 → 𝐵 ⊆ ∪ ∪ ran 𝑡 ) )
53 51 52 syl5com ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) → 𝐵 ⊆ ∪ ∪ ran 𝑡 ) )
54 53 ralimdva ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡 ) )
55 54 impr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡 )
56 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡 )
57 55 56 sylibr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡 )
58 57 adantlr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ∪ ran 𝑡 )
59 45 58 sstrd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → 𝐶 ⊆ ∪ ∪ ran 𝑡 )
60 unieq ⊢ ( 𝑣 = ∪ ran 𝑡 → ∪ 𝑣 = ∪ ∪ ran 𝑡 )
61 60 sseq2d ⊢ ( 𝑣 = ∪ ran 𝑡 → ( 𝐶 ⊆ ∪ 𝑣 ↔ 𝐶 ⊆ ∪ ∪ ran 𝑡 ) )
62 61 rspcev ⊢ ( ( ∪ ran 𝑡 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝐶 ⊆ ∪ ∪ ran 𝑡 ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐶 ⊆ ∪ 𝑣 )
63 44 59 62 syl2anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐶 ⊆ ∪ 𝑣 )
64 21 63 nsyl3 ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) ) → ¬ 𝐶 ∈ 𝐾 )
65 64 ex ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) → ¬ 𝐶 ∈ 𝐾 ) )
66 65 exlimdv ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ∃ 𝑡 ( 𝑡 : 𝐴 ⟶ ( 𝒫 𝑈 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ ( 𝑡 ‘ 𝑥 ) ) → ¬ 𝐶 ∈ 𝐾 ) )
67 16 66 syld ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝐵 ⊆ ∪ 𝑣 → ¬ 𝐶 ∈ 𝐾 ) )
68 11 67 biimtrid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ¬ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 → ¬ 𝐶 ∈ 𝐾 ) )
69 68 con4d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐶 ∈ 𝐾 → ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 ) )
70 69 3impia ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 )