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 \| \neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v\}$
	heiborlem1.4	$⊢ B \in V$
Assertion	heiborlem1	$⊢ (A \in Fin \land C \subseteq ⋃_{x \in A} B \land C \in K) \to \exists x \in A B \in K$

Proof

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

Metamath Proof Explorer

Theorem heiborlem1

Proof