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 ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐾 )