alexsubALTlem2

Description: Lemma for alexsubALT . Every subset of a base which has no finite subcover is a subset of a maximal such collection. (Contributed by Jeff Hankins, 27-Jan-2010)

		Ref	Expression
	Hypothesis	alexsubALT.1	$⊢ X = ⋃ J$
	Assertion	alexsubALTlem2	$⊢ ((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \to \exists u \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \forall v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \neg u \subset v$

Proof

Step	Hyp	Ref	Expression
1		alexsubALT.1	$⊢ X = ⋃ J$
2		ssel	$⊢ y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \to (w \in y \to w \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}))$
3		elun	$⊢ w \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \leftrightarrow (w \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \lor w \in \{\emptyset\})$
4		sseq2	$⊢ z = w \to (a \subseteq z \leftrightarrow a \subseteq w)$
5		pweq	$⊢ z = w \to 𝒫 z = 𝒫 w$
6	5	ineq1d	$⊢ z = w \to 𝒫 z \cap Fin = 𝒫 w \cap Fin$
7	6	raleqdv	$⊢ z = w \to (\forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b \leftrightarrow \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)$
8	4 7	anbi12d	$⊢ z = w \to ((a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b) \leftrightarrow (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b))$
9	8	elrab	$⊢ w \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \leftrightarrow (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b))$
10		velsn	$⊢ w \in \{\emptyset\} \leftrightarrow w = \emptyset$
11	9 10	orbi12i	$⊢ (w \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \lor w \in \{\emptyset\}) \leftrightarrow ((w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)) \lor w = \emptyset)$
12	3 11	bitri	$⊢ w \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \leftrightarrow ((w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)) \lor w = \emptyset)$
13		elpwi	$⊢ w \in 𝒫 fi (x) \to w \subseteq fi (x)$
14	13	adantr	$⊢ (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)) \to w \subseteq fi (x)$
15		0ss	$⊢ \emptyset \subseteq fi (x)$
16		sseq1	$⊢ w = \emptyset \to (w \subseteq fi (x) \leftrightarrow \emptyset \subseteq fi (x))$
17	15 16	mpbiri	$⊢ w = \emptyset \to w \subseteq fi (x)$
18	14 17	jaoi	$⊢ ((w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)) \lor w = \emptyset) \to w \subseteq fi (x)$
19	12 18	sylbi	$⊢ w \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \to w \subseteq fi (x)$
20	2 19	syl6	$⊢ y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \to (w \in y \to w \subseteq fi (x))$
21	20	ralrimiv	$⊢ y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \to \forall w \in y w \subseteq fi (x)$
22		unissb	$⊢ ⋃ y \subseteq fi (x) \leftrightarrow \forall w \in y w \subseteq fi (x)$
23	21 22	sylibr	$⊢ y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \to ⋃ y \subseteq fi (x)$
24	23	adantr	$⊢ (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y) \to ⋃ y \subseteq fi (x)$
25	24	ad2antlr	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to ⋃ y \subseteq fi (x)$
26		vuniex	$⊢ ⋃ y \in V$
27	26	elpw	$⊢ ⋃ y \in 𝒫 fi (x) \leftrightarrow ⋃ y \subseteq fi (x)$
28	25 27	sylibr	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to ⋃ y \in 𝒫 fi (x)$
29		uni0b	$⊢ ⋃ y = \emptyset \leftrightarrow y \subseteq \{\emptyset\}$
30	29	notbii	$⊢ \neg ⋃ y = \emptyset \leftrightarrow \neg y \subseteq \{\emptyset\}$
31		disjssun	$⊢ y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} = \emptyset \to (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \leftrightarrow y \subseteq \{\emptyset\})$
32	31	biimpcd	$⊢ y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \to (y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} = \emptyset \to y \subseteq \{\emptyset\})$
33	32	necon3bd	$⊢ y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \to (\neg y \subseteq \{\emptyset\} \to y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \neq \emptyset)$
34		n0	$⊢ y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \neq \emptyset \leftrightarrow \exists w w \in (y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\})$
35		elin	$⊢ w \in (y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}) \leftrightarrow (w \in y \land w \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\})$
36	9	anbi2i	$⊢ (w \in y \land w \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}) \leftrightarrow (w \in y \land (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)))$
37	35 36	bitri	$⊢ w \in (y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}) \leftrightarrow (w \in y \land (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)))$
38		simprrl	$⊢ (w \in y \land (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b))) \to a \subseteq w$
39		simpl	$⊢ (w \in y \land (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b))) \to w \in y$
40		ssuni	$⊢ (a \subseteq w \land w \in y) \to a \subseteq ⋃ y$
41	38 39 40	syl2anc	$⊢ (w \in y \land (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b))) \to a \subseteq ⋃ y$
42	37 41	sylbi	$⊢ w \in (y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}) \to a \subseteq ⋃ y$
43	42	exlimiv	$⊢ \exists w w \in (y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}) \to a \subseteq ⋃ y$
44	34 43	sylbi	$⊢ y \cap \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \neq \emptyset \to a \subseteq ⋃ y$
45	33 44	syl6	$⊢ y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \to (\neg y \subseteq \{\emptyset\} \to a \subseteq ⋃ y)$
46	45	ad2antrl	$⊢ (((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \to (\neg y \subseteq \{\emptyset\} \to a \subseteq ⋃ y)$
47	30 46	syl5bi	$⊢ (((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \to (\neg ⋃ y = \emptyset \to a \subseteq ⋃ y)$
48	47	imp	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to a \subseteq ⋃ y$
49		elfpw	$⊢ n \in (𝒫 ⋃ y \cap Fin) \leftrightarrow (n \subseteq ⋃ y \land n \in Fin)$
50		unieq	$⊢ y = \emptyset \to ⋃ y = ⋃ \emptyset$
51		uni0	$⊢ ⋃ \emptyset = \emptyset$
52	50 51	eqtrdi	$⊢ y = \emptyset \to ⋃ y = \emptyset$
53	52	necon3bi	$⊢ \neg ⋃ y = \emptyset \to y \neq \emptyset$
54	53	adantr	$⊢ (\neg ⋃ y = \emptyset \land n \in Fin) \to y \neq \emptyset$
55	54	ad2antrl	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land ((\neg ⋃ y = \emptyset \land n \in Fin) \land n \subseteq ⋃ y)) \to y \neq \emptyset$
56		simplrr	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land ((\neg ⋃ y = \emptyset \land n \in Fin) \land n \subseteq ⋃ y)) \to [\subset] Or y$
57		simprlr	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land ((\neg ⋃ y = \emptyset \land n \in Fin) \land n \subseteq ⋃ y)) \to n \in Fin$
58		simprr	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land ((\neg ⋃ y = \emptyset \land n \in Fin) \land n \subseteq ⋃ y)) \to n \subseteq ⋃ y$
59		finsschain	$⊢ ((y \neq \emptyset \land [\subset] Or y) \land (n \in Fin \land n \subseteq ⋃ y)) \to \exists w \in y n \subseteq w$
60	55 56 57 58 59	syl22anc	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land ((\neg ⋃ y = \emptyset \land n \in Fin) \land n \subseteq ⋃ y)) \to \exists w \in y n \subseteq w$
61	60	expr	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land (\neg ⋃ y = \emptyset \land n \in Fin)) \to (n \subseteq ⋃ y \to \exists w \in y n \subseteq w)$
62		0elpw	$⊢ \emptyset \in 𝒫 a$
63		0fin	$⊢ \emptyset \in Fin$
64	62 63	elini	$⊢ \emptyset \in (𝒫 a \cap Fin)$
65		unieq	$⊢ b = \emptyset \to ⋃ b = ⋃ \emptyset$
66	65	eqeq2d	$⊢ b = \emptyset \to (X = ⋃ b \leftrightarrow X = ⋃ \emptyset)$
67	66	notbid	$⊢ b = \emptyset \to (\neg X = ⋃ b \leftrightarrow \neg X = ⋃ \emptyset)$
68	67	rspccv	$⊢ \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \to (\emptyset \in (𝒫 a \cap Fin) \to \neg X = ⋃ \emptyset)$
69	64 68	mpi	$⊢ \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \to \neg X = ⋃ \emptyset$
70		velpw	$⊢ n \in 𝒫 w \leftrightarrow n \subseteq w$
71		elin	$⊢ n \in (𝒫 w \cap Fin) \leftrightarrow (n \in 𝒫 w \land n \in Fin)$
72		unieq	$⊢ b = n \to ⋃ b = ⋃ n$
73	72	eqeq2d	$⊢ b = n \to (X = ⋃ b \leftrightarrow X = ⋃ n)$
74	73	notbid	$⊢ b = n \to (\neg X = ⋃ b \leftrightarrow \neg X = ⋃ n)$
75	74	rspccv	$⊢ \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b \to (n \in (𝒫 w \cap Fin) \to \neg X = ⋃ n)$
76	71 75	syl5bir	$⊢ \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b \to ((n \in 𝒫 w \land n \in Fin) \to \neg X = ⋃ n)$
77	76	expd	$⊢ \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b \to (n \in 𝒫 w \to (n \in Fin \to \neg X = ⋃ n))$
78	70 77	syl5bir	$⊢ \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b \to (n \subseteq w \to (n \in Fin \to \neg X = ⋃ n))$
79	78	com23	$⊢ \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b \to (n \in Fin \to (n \subseteq w \to \neg X = ⋃ n))$
80	79	ad2antll	$⊢ (w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)) \to (n \in Fin \to (n \subseteq w \to \neg X = ⋃ n))$
81	80	a1i	$⊢ \neg X = ⋃ \emptyset \to ((w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)) \to (n \in Fin \to (n \subseteq w \to \neg X = ⋃ n)))$
82		sseq2	$⊢ w = \emptyset \to (n \subseteq w \leftrightarrow n \subseteq \emptyset)$
83		ss0	$⊢ n \subseteq \emptyset \to n = \emptyset$
84	82 83	syl6bi	$⊢ w = \emptyset \to (n \subseteq w \to n = \emptyset)$
85		unieq	$⊢ n = \emptyset \to ⋃ n = ⋃ \emptyset$
86	85	eqeq2d	$⊢ n = \emptyset \to (X = ⋃ n \leftrightarrow X = ⋃ \emptyset)$
87	86	notbid	$⊢ n = \emptyset \to (\neg X = ⋃ n \leftrightarrow \neg X = ⋃ \emptyset)$
88	87	biimprcd	$⊢ \neg X = ⋃ \emptyset \to (n = \emptyset \to \neg X = ⋃ n)$
89	88	a1dd	$⊢ \neg X = ⋃ \emptyset \to (n = \emptyset \to (n \in Fin \to \neg X = ⋃ n))$
90	84 89	syl9r	$⊢ \neg X = ⋃ \emptyset \to (w = \emptyset \to (n \subseteq w \to (n \in Fin \to \neg X = ⋃ n)))$
91	90	com34	$⊢ \neg X = ⋃ \emptyset \to (w = \emptyset \to (n \in Fin \to (n \subseteq w \to \neg X = ⋃ n)))$
92	81 91	jaod	$⊢ \neg X = ⋃ \emptyset \to (((w \in 𝒫 fi (x) \land (a \subseteq w \land \forall b \in (𝒫 w \cap Fin) \neg X = ⋃ b)) \lor w = \emptyset) \to (n \in Fin \to (n \subseteq w \to \neg X = ⋃ n)))$
93	12 92	syl5bi	$⊢ \neg X = ⋃ \emptyset \to (w \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \to (n \in Fin \to (n \subseteq w \to \neg X = ⋃ n)))$
94	2 93	sylan9r	$⊢ (\neg X = ⋃ \emptyset \land y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \to (w \in y \to (n \in Fin \to (n \subseteq w \to \neg X = ⋃ n)))$
95	94	com23	$⊢ (\neg X = ⋃ \emptyset \land y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \to (n \in Fin \to (w \in y \to (n \subseteq w \to \neg X = ⋃ n)))$
96	69 95	sylan	$⊢ (\forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \land y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \to (n \in Fin \to (w \in y \to (n \subseteq w \to \neg X = ⋃ n)))$
97	96	ad2ant2lr	$⊢ (((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \to (n \in Fin \to (w \in y \to (n \subseteq w \to \neg X = ⋃ n)))$
98	97	imp	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land n \in Fin) \to (w \in y \to (n \subseteq w \to \neg X = ⋃ n))$
99	98	adantrl	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land (\neg ⋃ y = \emptyset \land n \in Fin)) \to (w \in y \to (n \subseteq w \to \neg X = ⋃ n))$
100	99	rexlimdv	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land (\neg ⋃ y = \emptyset \land n \in Fin)) \to (\exists w \in y n \subseteq w \to \neg X = ⋃ n)$
101	61 100	syld	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land (\neg ⋃ y = \emptyset \land n \in Fin)) \to (n \subseteq ⋃ y \to \neg X = ⋃ n)$
102	101	expr	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to (n \in Fin \to (n \subseteq ⋃ y \to \neg X = ⋃ n))$
103	102	impcomd	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to ((n \subseteq ⋃ y \land n \in Fin) \to \neg X = ⋃ n)$
104	49 103	syl5bi	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to (n \in (𝒫 ⋃ y \cap Fin) \to \neg X = ⋃ n)$
105	104	ralrimiv	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to \forall n \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ n$
106		unieq	$⊢ n = b \to ⋃ n = ⋃ b$
107	106	eqeq2d	$⊢ n = b \to (X = ⋃ n \leftrightarrow X = ⋃ b)$
108	107	notbid	$⊢ n = b \to (\neg X = ⋃ n \leftrightarrow \neg X = ⋃ b)$
109	108	cbvralvw	$⊢ \forall n \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ n \leftrightarrow \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b$
110	105 109	sylib	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b$
111	28 48 110	jca32	$⊢ ((((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \land \neg ⋃ y = \emptyset) \to (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b))$
112	111	ex	$⊢ (((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \to (\neg ⋃ y = \emptyset \to (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b)))$
113		orcom	$⊢ (⋃ y \in \{\emptyset\} \lor ⋃ y \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}) \leftrightarrow (⋃ y \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \lor ⋃ y \in \{\emptyset\})$
114	26	elsn	$⊢ ⋃ y \in \{\emptyset\} \leftrightarrow ⋃ y = \emptyset$
115		sseq2	$⊢ z = ⋃ y \to (a \subseteq z \leftrightarrow a \subseteq ⋃ y)$
116		pweq	$⊢ z = ⋃ y \to 𝒫 z = 𝒫 ⋃ y$
117	116	ineq1d	$⊢ z = ⋃ y \to 𝒫 z \cap Fin = 𝒫 ⋃ y \cap Fin$
118	117	raleqdv	$⊢ z = ⋃ y \to (\forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b \leftrightarrow \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b)$
119	115 118	anbi12d	$⊢ z = ⋃ y \to ((a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b) \leftrightarrow (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b))$
120	119	elrab	$⊢ ⋃ y \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \leftrightarrow (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b))$
121	114 120	orbi12i	$⊢ (⋃ y \in \{\emptyset\} \lor ⋃ y \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}) \leftrightarrow (⋃ y = \emptyset \lor (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b)))$
122		df-or	$⊢ (⋃ y = \emptyset \lor (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b))) \leftrightarrow (\neg ⋃ y = \emptyset \to (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b)))$
123	121 122	bitr2i	$⊢ (\neg ⋃ y = \emptyset \to (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b))) \leftrightarrow (⋃ y \in \{\emptyset\} \lor ⋃ y \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\})$
124		elun	$⊢ ⋃ y \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \leftrightarrow (⋃ y \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \lor ⋃ y \in \{\emptyset\})$
125	113 123 124	3bitr4i	$⊢ (\neg ⋃ y = \emptyset \to (⋃ y \in 𝒫 fi (x) \land (a \subseteq ⋃ y \land \forall b \in (𝒫 ⋃ y \cap Fin) \neg X = ⋃ b))) \leftrightarrow ⋃ y \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\})$
126	112 125	sylib	$⊢ (((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \land (y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y)) \to ⋃ y \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\})$
127	126	ex	$⊢ ((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \to ((y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y) \to ⋃ y \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}))$
128	127	alrimiv	$⊢ ((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \to \forall y ((y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y) \to ⋃ y \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}))$
129		fvex	$⊢ fi (x) \in V$
130	129	pwex	$⊢ 𝒫 fi (x) \in V$
131	130	rabex	$⊢ \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \in V$
132		p0ex	$⊢ \{\emptyset\} \in V$
133	131 132	unex	$⊢ \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \in V$
134	133	zorn	$⊢ \forall y ((y \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\} \land [\subset] Or y) \to ⋃ y \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\})) \to \exists u \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \forall v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \neg u \subset v$
135	128 134	syl	$⊢ ((J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \land a \in 𝒫 fi (x)) \land \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \to \exists u \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \forall v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \neg u \subset v$

Metamath Proof Explorer

Theorem alexsubALTlem2

Proof