alexsubALTlem3

Description: Lemma for alexsubALT . If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010) (Revised by Mario Carneiro, 14-Dec-2013)

		Ref	Expression
	Hypothesis	alexsubALT.1	$⊢ X = ⋃ J$
	Assertion	alexsubALTlem3	$⊢ ((((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 (u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \land w \in u) \land ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u)))) \to \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n$

Proof

Step	Hyp	Ref	Expression
1		alexsubALT.1	$⊢ X = ⋃ J$
2		dfrex2	$⊢ \exists n \in (𝒫 (u \cup \{s\}) \cap Fin) X = ⋃ n \leftrightarrow \neg \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n$
3	2	ralbii	$⊢ \forall s \in t \exists n \in (𝒫 (u \cup \{s\}) \cap Fin) X = ⋃ n \leftrightarrow \forall s \in t \neg \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n$
4		ralnex	$⊢ \forall s \in t \neg \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n \leftrightarrow \neg \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n$
5	3 4	bitr2i	$⊢ \neg \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n \leftrightarrow \forall s \in t \exists n \in (𝒫 (u \cup \{s\}) \cap Fin) X = ⋃ n$
6		elin	$⊢ n \in (𝒫 (u \cup \{s\}) \cap Fin) \leftrightarrow (n \in 𝒫 (u \cup \{s\}) \land n \in Fin)$
7		elpwi	$⊢ n \in 𝒫 (u \cup \{s\}) \to n \subseteq u \cup \{s\}$
8	7	adantr	$⊢ (n \in 𝒫 (u \cup \{s\}) \land n \in Fin) \to n \subseteq u \cup \{s\}$
9		uncom	$⊢ u \cup \{s\} = \{s\} \cup u$
10	8 9	sseqtrdi	$⊢ (n \in 𝒫 (u \cup \{s\}) \land n \in Fin) \to n \subseteq \{s\} \cup u$
11		ssundif	$⊢ n \subseteq \{s\} \cup u \leftrightarrow n ∖ \{s\} \subseteq u$
12	10 11	sylib	$⊢ (n \in 𝒫 (u \cup \{s\}) \land n \in Fin) \to n ∖ \{s\} \subseteq u$
13		diffi	$⊢ n \in Fin \to n ∖ \{s\} \in Fin$
14	13	adantl	$⊢ (n \in 𝒫 (u \cup \{s\}) \land n \in Fin) \to n ∖ \{s\} \in Fin$
15	12 14	jca	$⊢ (n \in 𝒫 (u \cup \{s\}) \land n \in Fin) \to (n ∖ \{s\} \subseteq u \land n ∖ \{s\} \in Fin)$
16	6 15	sylbi	$⊢ n \in (𝒫 (u \cup \{s\}) \cap Fin) \to (n ∖ \{s\} \subseteq u \land n ∖ \{s\} \in Fin)$
17	16	adantr	$⊢ (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n) \to (n ∖ \{s\} \subseteq u \land n ∖ \{s\} \in Fin)$
18	17	ad2antll	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to (n ∖ \{s\} \subseteq u \land n ∖ \{s\} \in Fin)$
19		elin	$⊢ n ∖ \{s\} \in (𝒫 u \cap Fin) \leftrightarrow (n ∖ \{s\} \in 𝒫 u \land n ∖ \{s\} \in Fin)$
20		vex	$⊢ u \in V$
21	20	elpw2	$⊢ n ∖ \{s\} \in 𝒫 u \leftrightarrow n ∖ \{s\} \subseteq u$
22	21	anbi1i	$⊢ (n ∖ \{s\} \in 𝒫 u \land n ∖ \{s\} \in Fin) \leftrightarrow (n ∖ \{s\} \subseteq u \land n ∖ \{s\} \in Fin)$
23	19 22	bitr2i	$⊢ (n ∖ \{s\} \subseteq u \land n ∖ \{s\} \in Fin) \leftrightarrow n ∖ \{s\} \in (𝒫 u \cap Fin)$
24	18 23	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to n ∖ \{s\} \in (𝒫 u \cap Fin)$
25		simprrr	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to X = ⋃ n$
26		eldif	$⊢ x \in (n ∖ \{s\}) \leftrightarrow (x \in n \land \neg x \in \{s\})$
27	26	simplbi2	$⊢ x \in n \to (\neg x \in \{s\} \to x \in (n ∖ \{s\}))$
28		elun	$⊢ x \in ((n ∖ \{s\}) \cup \{s\}) \leftrightarrow (x \in (n ∖ \{s\}) \lor x \in \{s\})$
29		orcom	$⊢ (x \in \{s\} \lor x \in (n ∖ \{s\})) \leftrightarrow (x \in (n ∖ \{s\}) \lor x \in \{s\})$
30	28 29	bitr4i	$⊢ x \in ((n ∖ \{s\}) \cup \{s\}) \leftrightarrow (x \in \{s\} \lor x \in (n ∖ \{s\}))$
31		df-or	$⊢ (x \in \{s\} \lor x \in (n ∖ \{s\})) \leftrightarrow (\neg x \in \{s\} \to x \in (n ∖ \{s\}))$
32	30 31	bitr2i	$⊢ (\neg x \in \{s\} \to x \in (n ∖ \{s\})) \leftrightarrow x \in ((n ∖ \{s\}) \cup \{s\})$
33	27 32	sylib	$⊢ x \in n \to x \in ((n ∖ \{s\}) \cup \{s\})$
34	33	ssriv	$⊢ n \subseteq (n ∖ \{s\}) \cup \{s\}$
35		uniss	$⊢ n \subseteq (n ∖ \{s\}) \cup \{s\} \to ⋃ n \subseteq ⋃ ((n ∖ \{s\}) \cup \{s\})$
36	34 35	mp1i	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ n \subseteq ⋃ ((n ∖ \{s\}) \cup \{s\})$
37		uniun	$⊢ ⋃ ((n ∖ \{s\}) \cup \{s\}) = ⋃ (n ∖ \{s\}) \cup ⋃ \{s\}$
38		unisnv	$⊢ ⋃ \{s\} = s$
39	38	uneq2i	$⊢ ⋃ (n ∖ \{s\}) \cup ⋃ \{s\} = ⋃ (n ∖ \{s\}) \cup s$
40	37 39	eqtri	$⊢ ⋃ ((n ∖ \{s\}) \cup \{s\}) = ⋃ (n ∖ \{s\}) \cup s$
41	36 40	sseqtrdi	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ n \subseteq ⋃ (n ∖ \{s\}) \cup s$
42	25 41	eqsstrd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to X \subseteq ⋃ (n ∖ \{s\}) \cup s$
43		difss	$⊢ n ∖ \{s\} \subseteq n$
44	43	unissi	$⊢ ⋃ (n ∖ \{s\}) \subseteq ⋃ n$
45		sseq2	$⊢ X = ⋃ n \to (⋃ (n ∖ \{s\}) \subseteq X \leftrightarrow ⋃ (n ∖ \{s\}) \subseteq ⋃ n)$
46	44 45	mpbiri	$⊢ X = ⋃ n \to ⋃ (n ∖ \{s\}) \subseteq X$
47	46	adantl	$⊢ (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n) \to ⋃ (n ∖ \{s\}) \subseteq X$
48	47	ad2antll	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ (n ∖ \{s\}) \subseteq X$
49		elinel1	$⊢ t \in (𝒫 x \cap Fin) \to t \in 𝒫 x$
50	49	elpwid	$⊢ t \in (𝒫 x \cap Fin) \to t \subseteq x$
51	50	ad3antrrr	$⊢ (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u) \to t \subseteq x$
52	51	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to t \subseteq x$
53		simprl	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to s \in t$
54	52 53	sseldd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to s \in x$
55		elssuni	$⊢ s \in x \to s \subseteq ⋃ x$
56	54 55	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to s \subseteq ⋃ x$
57		fibas	$⊢ fi (x) \in TopBases$
58		unitg	$⊢ fi (x) \in TopBases \to ⋃ topGen (fi (x)) = ⋃ fi (x)$
59	57 58	mp1i	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ topGen (fi (x)) = ⋃ fi (x)$
60		unieq	$⊢ J = topGen (fi (x)) \to ⋃ J = ⋃ topGen (fi (x))$
61	60	3ad2ant1	$⊢ (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)) \to ⋃ J = ⋃ topGen (fi (x))$
62	61	ad3antrrr	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ J = ⋃ topGen (fi (x))$
63		vex	$⊢ x \in V$
64		fiuni	$⊢ x \in V \to ⋃ x = ⋃ fi (x)$
65	63 64	mp1i	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ x = ⋃ fi (x)$
66	59 62 65	3eqtr4rd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ x = ⋃ J$
67	66 1	eqtr4di	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ x = X$
68	56 67	sseqtrd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to s \subseteq X$
69	48 68	unssd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to ⋃ (n ∖ \{s\}) \cup s \subseteq X$
70	42 69	eqssd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to X = ⋃ (n ∖ \{s\}) \cup s$
71		unieq	$⊢ m = n ∖ \{s\} \to ⋃ m = ⋃ (n ∖ \{s\})$
72	71	uneq1d	$⊢ m = n ∖ \{s\} \to ⋃ m \cup s = ⋃ (n ∖ \{s\}) \cup s$
73	72	rspceeqv	$⊢ (n ∖ \{s\} \in (𝒫 u \cap Fin) \land X = ⋃ (n ∖ \{s\}) \cup s) \to \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s$
74	24 70 73	syl2anc	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (s \in t \land (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n))) \to \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s$
75	74	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land s \in t) \to ((n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n) \to \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s)$
76	75	expd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land s \in t) \to (n \in (𝒫 (u \cup \{s\}) \cap Fin) \to (X = ⋃ n \to \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s))$
77	76	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land s \in t) \to (\exists n \in (𝒫 (u \cup \{s\}) \cap Fin) X = ⋃ n \to \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s)$
78	77	ralimdva	$⊢ (((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to (\forall s \in t \exists n \in (𝒫 (u \cup \{s\}) \cap Fin) X = ⋃ n \to \forall s \in t \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s)$
79		elinel2	$⊢ t \in (𝒫 x \cap Fin) \to t \in Fin$
80	79	adantr	$⊢ (t \in (𝒫 x \cap Fin) \land w = ⋂ t) \to t \in Fin$
81		unieq	$⊢ m = f (s) \to ⋃ m = ⋃ f (s)$
82	81	uneq1d	$⊢ m = f (s) \to ⋃ m \cup s = ⋃ f (s) \cup s$
83	82	eqeq2d	$⊢ m = f (s) \to (X = ⋃ m \cup s \leftrightarrow X = ⋃ f (s) \cup s)$
84	83	ac6sfi	$⊢ (t \in Fin \land \forall s \in t \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s) \to \exists f (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)$
85	84	ex	$⊢ t \in Fin \to (\forall s \in t \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s \to \exists f (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s))$
86	80 85	syl	$⊢ (t \in (𝒫 x \cap Fin) \land w = ⋂ t) \to (\forall s \in t \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s \to \exists f (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s))$
87	86	adantr	$⊢ ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \to (\forall s \in t \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s \to \exists f (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s))$
88	87	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to (\forall s \in t \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s \to \exists f (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s))$
89		ffvelcdm	$⊢ (f : t ⟶ 𝒫 u \cap Fin \land s \in t) \to f (s) \in (𝒫 u \cap Fin)$
90		elin	$⊢ f (s) \in (𝒫 u \cap Fin) \leftrightarrow (f (s) \in 𝒫 u \land f (s) \in Fin)$
91		elpwi	$⊢ f (s) \in 𝒫 u \to f (s) \subseteq u$
92	91	adantr	$⊢ (f (s) \in 𝒫 u \land f (s) \in Fin) \to f (s) \subseteq u$
93	90 92	sylbi	$⊢ f (s) \in (𝒫 u \cap Fin) \to f (s) \subseteq u$
94	89 93	syl	$⊢ (f : t ⟶ 𝒫 u \cap Fin \land s \in t) \to f (s) \subseteq u$
95	94	ralrimiva	$⊢ f : t ⟶ 𝒫 u \cap Fin \to \forall s \in t f (s) \subseteq u$
96		iunss	$⊢ ⋃_{s \in t} f (s) \subseteq u \leftrightarrow \forall s \in t f (s) \subseteq u$
97	95 96	sylibr	$⊢ f : t ⟶ 𝒫 u \cap Fin \to ⋃_{s \in t} f (s) \subseteq u$
98	97	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ⋃_{s \in t} f (s) \subseteq u$
99		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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to w \in u$
100	99	snssd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to \{w\} \subseteq u$
101	98 100	unssd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ⋃_{s \in t} f (s) \cup \{w\} \subseteq u$
102	89	elin2d	$⊢ (f : t ⟶ 𝒫 u \cap Fin \land s \in t) \to f (s) \in Fin$
103	102	ralrimiva	$⊢ f : t ⟶ 𝒫 u \cap Fin \to \forall s \in t f (s) \in Fin$
104		iunfi	$⊢ (t \in Fin \land \forall s \in t f (s) \in Fin) \to ⋃_{s \in t} f (s) \in Fin$
105	80 103 104	syl2an	$⊢ ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land f : t ⟶ 𝒫 u \cap Fin) \to ⋃_{s \in t} f (s) \in Fin$
106	105	ad4ant14	$⊢ ((((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u) \land f : t ⟶ 𝒫 u \cap Fin) \to ⋃_{s \in t} f (s) \in Fin$
107	106	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ⋃_{s \in t} f (s) \in Fin$
108		snfi	$⊢ \{w\} \in Fin$
109		unfi	$⊢ (⋃_{s \in t} f (s) \in Fin \land \{w\} \in Fin) \to ⋃_{s \in t} f (s) \cup \{w\} \in Fin$
110	107 108 109	sylancl	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ⋃_{s \in t} f (s) \cup \{w\} \in Fin$
111	101 110	jca	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to (⋃_{s \in t} f (s) \cup \{w\} \subseteq u \land ⋃_{s \in t} f (s) \cup \{w\} \in Fin)$
112		elin	$⊢ ⋃_{s \in t} f (s) \cup \{w\} \in (𝒫 u \cap Fin) \leftrightarrow (⋃_{s \in t} f (s) \cup \{w\} \in 𝒫 u \land ⋃_{s \in t} f (s) \cup \{w\} \in Fin)$
113	20	elpw2	$⊢ ⋃_{s \in t} f (s) \cup \{w\} \in 𝒫 u \leftrightarrow ⋃_{s \in t} f (s) \cup \{w\} \subseteq u$
114	113	anbi1i	$⊢ (⋃_{s \in t} f (s) \cup \{w\} \in 𝒫 u \land ⋃_{s \in t} f (s) \cup \{w\} \in Fin) \leftrightarrow (⋃_{s \in t} f (s) \cup \{w\} \subseteq u \land ⋃_{s \in t} f (s) \cup \{w\} \in Fin)$
115	112 114	bitr2i	$⊢ (⋃_{s \in t} f (s) \cup \{w\} \subseteq u \land ⋃_{s \in t} f (s) \cup \{w\} \in Fin) \leftrightarrow ⋃_{s \in t} f (s) \cup \{w\} \in (𝒫 u \cap Fin)$
116	111 115	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ⋃_{s \in t} f (s) \cup \{w\} \in (𝒫 u \cap Fin)$
117		ralnex	$⊢ \forall s \in t \neg y \in f (s) \leftrightarrow \neg \exists s \in t y \in f (s)$
118	117	imbi2i	$⊢ (v \in y \to \forall s \in t \neg y \in f (s)) \leftrightarrow (v \in y \to \neg \exists s \in t y \in f (s))$
119	118	albii	$⊢ \forall y (v \in y \to \forall s \in t \neg y \in f (s)) \leftrightarrow \forall y (v \in y \to \neg \exists s \in t y \in f (s))$
120		alinexa	$⊢ \forall y (v \in y \to \neg \exists s \in t y \in f (s)) \leftrightarrow \neg \exists y (v \in y \land \exists s \in t y \in f (s))$
121	119 120	bitr2i	$⊢ \neg \exists y (v \in y \land \exists s \in t y \in f (s)) \leftrightarrow \forall y (v \in y \to \forall s \in t \neg y \in f (s))$
122		fveq2	$⊢ s = z \to f (s) = f (z)$
123	122	unieqd	$⊢ s = z \to ⋃ f (s) = ⋃ f (z)$
124		id	$⊢ s = z \to s = z$
125	123 124	uneq12d	$⊢ s = z \to ⋃ f (s) \cup s = ⋃ f (z) \cup z$
126	125	eqeq2d	$⊢ s = z \to (X = ⋃ f (s) \cup s \leftrightarrow X = ⋃ f (z) \cup z)$
127	126	rspcv	$⊢ z \in t \to (\forall s \in t X = ⋃ f (s) \cup s \to X = ⋃ f (z) \cup z)$
128		eleq2	$⊢ X = ⋃ f (z) \cup z \to (v \in X \leftrightarrow v \in (⋃ f (z) \cup z))$
129	128	biimpd	$⊢ X = ⋃ f (z) \cup z \to (v \in X \to v \in (⋃ f (z) \cup z))$
130		elun	$⊢ v \in (⋃ f (z) \cup z) \leftrightarrow (v \in ⋃ f (z) \lor v \in z)$
131		eluni	$⊢ v \in ⋃ f (z) \leftrightarrow \exists w (v \in w \land w \in f (z))$
132	131	orbi1i	$⊢ (v \in ⋃ f (z) \lor v \in z) \leftrightarrow (\exists w (v \in w \land w \in f (z)) \lor v \in z)$
133		df-or	$⊢ (\exists w (v \in w \land w \in f (z)) \lor v \in z) \leftrightarrow (\neg \exists w (v \in w \land w \in f (z)) \to v \in z)$
134		alinexa	$⊢ \forall w (v \in w \to \neg w \in f (z)) \leftrightarrow \neg \exists w (v \in w \land w \in f (z))$
135	134	imbi1i	$⊢ (\forall w (v \in w \to \neg w \in f (z)) \to v \in z) \leftrightarrow (\neg \exists w (v \in w \land w \in f (z)) \to v \in z)$
136	133 135	bitr4i	$⊢ (\exists w (v \in w \land w \in f (z)) \lor v \in z) \leftrightarrow (\forall w (v \in w \to \neg w \in f (z)) \to v \in z)$
137	130 132 136	3bitri	$⊢ v \in (⋃ f (z) \cup z) \leftrightarrow (\forall w (v \in w \to \neg w \in f (z)) \to v \in z)$
138		eleq2	$⊢ y = w \to (v \in y \leftrightarrow v \in w)$
139		eleq1w	$⊢ y = w \to (y \in f (s) \leftrightarrow w \in f (s))$
140	139	notbid	$⊢ y = w \to (\neg y \in f (s) \leftrightarrow \neg w \in f (s))$
141	140	ralbidv	$⊢ y = w \to (\forall s \in t \neg y \in f (s) \leftrightarrow \forall s \in t \neg w \in f (s))$
142	138 141	imbi12d	$⊢ y = w \to ((v \in y \to \forall s \in t \neg y \in f (s)) \leftrightarrow (v \in w \to \forall s \in t \neg w \in f (s)))$
143	142	spvv	$⊢ \forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to (v \in w \to \forall s \in t \neg w \in f (s))$
144	122	eleq2d	$⊢ s = z \to (w \in f (s) \leftrightarrow w \in f (z))$
145	144	notbid	$⊢ s = z \to (\neg w \in f (s) \leftrightarrow \neg w \in f (z))$
146	145	rspcv	$⊢ z \in t \to (\forall s \in t \neg w \in f (s) \to \neg w \in f (z))$
147	143 146	syl9r	$⊢ z \in t \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to (v \in w \to \neg w \in f (z)))$
148	147	alrimdv	$⊢ z \in t \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to \forall w (v \in w \to \neg w \in f (z)))$
149	148	imim1d	$⊢ z \in t \to ((\forall w (v \in w \to \neg w \in f (z)) \to v \in z) \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in z))$
150	137 149	biimtrid	$⊢ z \in t \to (v \in (⋃ f (z) \cup z) \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in z))$
151	150	a1dd	$⊢ z \in t \to (v \in (⋃ f (z) \cup z) \to (w = ⋂ t \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in z)))$
152	129 151	syl9r	$⊢ z \in t \to (X = ⋃ f (z) \cup z \to (v \in X \to (w = ⋂ t \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in z))))$
153	127 152	syld	$⊢ z \in t \to (\forall s \in t X = ⋃ f (s) \cup s \to (v \in X \to (w = ⋂ t \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in z))))$
154	153	com14	$⊢ w = ⋂ t \to (\forall s \in t X = ⋃ f (s) \cup s \to (v \in X \to (z \in t \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in z))))$
155	154	imp31	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (z \in t \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in z))$
156	155	com23	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to (z \in t \to v \in z))$
157	156	ralrimdv	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to \forall z \in t v \in z)$
158		vex	$⊢ v \in V$
159	158	elint2	$⊢ v \in ⋂ t \leftrightarrow \forall z \in t v \in z$
160	157 159	syl6ibr	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in ⋂ t)$
161		eleq2	$⊢ w = ⋂ t \to (v \in w \leftrightarrow v \in ⋂ t)$
162	161	ad2antrr	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (v \in w \leftrightarrow v \in ⋂ t)$
163	160 162	sylibrd	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (\forall y (v \in y \to \forall s \in t \neg y \in f (s)) \to v \in w)$
164	121 163	biimtrid	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (\neg \exists y (v \in y \land \exists s \in t y \in f (s)) \to v \in w)$
165	164	orrd	$⊢ ((w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \land v \in X) \to (\exists y (v \in y \land \exists s \in t y \in f (s)) \lor v \in w)$
166	165	ex	$⊢ (w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \to (v \in X \to (\exists y (v \in y \land \exists s \in t y \in f (s)) \lor v \in w))$
167		orc	$⊢ \exists s \in t y \in f (s) \to (\exists s \in t y \in f (s) \lor y = w)$
168	167	anim2i	$⊢ (v \in y \land \exists s \in t y \in f (s)) \to (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
169	168	eximi	$⊢ \exists y (v \in y \land \exists s \in t y \in f (s)) \to \exists y (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
170		equid	$⊢ w = w$
171		vex	$⊢ w \in V$
172		equequ1	$⊢ y = w \to (y = w \leftrightarrow w = w)$
173	138 172	anbi12d	$⊢ y = w \to ((v \in y \land y = w) \leftrightarrow (v \in w \land w = w))$
174	171 173	spcev	$⊢ (v \in w \land w = w) \to \exists y (v \in y \land y = w)$
175	170 174	mpan2	$⊢ v \in w \to \exists y (v \in y \land y = w)$
176		olc	$⊢ y = w \to (\exists s \in t y \in f (s) \lor y = w)$
177	176	anim2i	$⊢ (v \in y \land y = w) \to (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
178	177	eximi	$⊢ \exists y (v \in y \land y = w) \to \exists y (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
179	175 178	syl	$⊢ v \in w \to \exists y (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
180	169 179	jaoi	$⊢ (\exists y (v \in y \land \exists s \in t y \in f (s)) \lor v \in w) \to \exists y (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
181		eluni	$⊢ v \in ⋃ (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow \exists y (v \in y \land y \in (⋃_{s \in t} f (s) \cup \{w\}))$
182		elun	$⊢ y \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (y \in ⋃_{s \in t} f (s) \lor y \in \{w\})$
183		eliun	$⊢ y \in ⋃_{s \in t} f (s) \leftrightarrow \exists s \in t y \in f (s)$
184		velsn	$⊢ y \in \{w\} \leftrightarrow y = w$
185	183 184	orbi12i	$⊢ (y \in ⋃_{s \in t} f (s) \lor y \in \{w\}) \leftrightarrow (\exists s \in t y \in f (s) \lor y = w)$
186	182 185	bitri	$⊢ y \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (\exists s \in t y \in f (s) \lor y = w)$
187	186	anbi2i	$⊢ (v \in y \land y \in (⋃_{s \in t} f (s) \cup \{w\})) \leftrightarrow (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
188	187	exbii	$⊢ \exists y (v \in y \land y \in (⋃_{s \in t} f (s) \cup \{w\})) \leftrightarrow \exists y (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
189	181 188	bitr2i	$⊢ \exists y (v \in y \land (\exists s \in t y \in f (s) \lor y = w)) \leftrightarrow v \in ⋃ (⋃_{s \in t} f (s) \cup \{w\})$
190	180 189	sylib	$⊢ (\exists y (v \in y \land \exists s \in t y \in f (s)) \lor v \in w) \to v \in ⋃ (⋃_{s \in t} f (s) \cup \{w\})$
191	166 190	syl6	$⊢ (w = ⋂ t \land \forall s \in t X = ⋃ f (s) \cup s) \to (v \in X \to v \in ⋃ (⋃_{s \in t} f (s) \cup \{w\}))$
192	191	ad5ant25	$⊢ ((((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u) \land \forall s \in t X = ⋃ f (s) \cup s) \to (v \in X \to v \in ⋃ (⋃_{s \in t} f (s) \cup \{w\}))$
193	192	ad2ant2l	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to (v \in X \to v \in ⋃ (⋃_{s \in t} f (s) \cup \{w\}))$
194	193	ssrdv	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to X \subseteq ⋃ (⋃_{s \in t} f (s) \cup \{w\})$
195		elun	$⊢ v \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (v \in ⋃_{s \in t} f (s) \lor v \in \{w\})$
196		eliun	$⊢ v \in ⋃_{s \in t} f (s) \leftrightarrow \exists s \in t v \in f (s)$
197		velsn	$⊢ v \in \{w\} \leftrightarrow v = w$
198	196 197	orbi12i	$⊢ (v \in ⋃_{s \in t} f (s) \lor v \in \{w\}) \leftrightarrow (\exists s \in t v \in f (s) \lor v = w)$
199	195 198	bitri	$⊢ v \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (\exists s \in t v \in f (s) \lor v = w)$
200		nfra1	$⊢ Ⅎ s \forall s \in t X = ⋃ f (s) \cup s$
201		nfv	$⊢ Ⅎ s v \subseteq X$
202		rsp	$⊢ \forall s \in t X = ⋃ f (s) \cup s \to (s \in t \to X = ⋃ f (s) \cup s)$
203		eqimss2	$⊢ X = ⋃ f (s) \cup s \to ⋃ f (s) \cup s \subseteq X$
204		elssuni	$⊢ v \in f (s) \to v \subseteq ⋃ f (s)$
205		ssun3	$⊢ v \subseteq ⋃ f (s) \to v \subseteq ⋃ f (s) \cup s$
206	204 205	syl	$⊢ v \in f (s) \to v \subseteq ⋃ f (s) \cup s$
207		sstr	$⊢ (v \subseteq ⋃ f (s) \cup s \land ⋃ f (s) \cup s \subseteq X) \to v \subseteq X$
208	207	expcom	$⊢ ⋃ f (s) \cup s \subseteq X \to (v \subseteq ⋃ f (s) \cup s \to v \subseteq X)$
209	203 206 208	syl2im	$⊢ X = ⋃ f (s) \cup s \to (v \in f (s) \to v \subseteq X)$
210	202 209	syl6	$⊢ \forall s \in t X = ⋃ f (s) \cup s \to (s \in t \to (v \in f (s) \to v \subseteq X))$
211	200 201 210	rexlimd	$⊢ \forall s \in t X = ⋃ f (s) \cup s \to (\exists s \in t v \in f (s) \to v \subseteq X)$
212	211	ad2antll	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to (\exists s \in t v \in f (s) \to v \subseteq X)$
213		elpwi	$⊢ u \in 𝒫 fi (x) \to u \subseteq fi (x)$
214	213	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \to u \subseteq fi (x)$
215	214	ad2antrr	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to u \subseteq fi (x)$
216	215 99	sseldd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to w \in fi (x)$
217		elssuni	$⊢ w \in fi (x) \to w \subseteq ⋃ fi (x)$
218	216 217	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to w \subseteq ⋃ fi (x)$
219	57 58	ax-mp	$⊢ ⋃ topGen (fi (x)) = ⋃ fi (x)$
220	60 219	eqtr2di	$⊢ J = topGen (fi (x)) \to ⋃ fi (x) = ⋃ J$
221	220 1	eqtr4di	$⊢ J = topGen (fi (x)) \to ⋃ fi (x) = X$
222	221	3ad2ant1	$⊢ (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)) \to ⋃ fi (x) = X$
223	222	ad3antrrr	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ⋃ fi (x) = X$
224	218 223	sseqtrd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to w \subseteq X$
225		sseq1	$⊢ v = w \to (v \subseteq X \leftrightarrow w \subseteq X)$
226	224 225	syl5ibrcom	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to (v = w \to v \subseteq X)$
227	212 226	jaod	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ((\exists s \in t v \in f (s) \lor v = w) \to v \subseteq X)$
228	199 227	biimtrid	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to (v \in (⋃_{s \in t} f (s) \cup \{w\}) \to v \subseteq X)$
229	228	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to \forall v \in (⋃_{s \in t} f (s) \cup \{w\}) v \subseteq X$
230		unissb	$⊢ ⋃ (⋃_{s \in t} f (s) \cup \{w\}) \subseteq X \leftrightarrow \forall v \in (⋃_{s \in t} f (s) \cup \{w\}) v \subseteq X$
231	229 230	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to ⋃ (⋃_{s \in t} f (s) \cup \{w\}) \subseteq X$
232	194 231	eqssd	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to X = ⋃ (⋃_{s \in t} f (s) \cup \{w\})$
233		unieq	$⊢ b = ⋃_{s \in t} f (s) \cup \{w\} \to ⋃ b = ⋃ (⋃_{s \in t} f (s) \cup \{w\})$
234	233	rspceeqv	$⊢ (⋃_{s \in t} f (s) \cup \{w\} \in (𝒫 u \cap Fin) \land X = ⋃ (⋃_{s \in t} f (s) \cup \{w\})) \to \exists b \in (𝒫 u \cap Fin) X = ⋃ b$
235	116 232 234	syl2anc	$⊢ ((((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \land (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s)) \to \exists b \in (𝒫 u \cap Fin) X = ⋃ b$
236	235	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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to ((f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s) \to \exists b \in (𝒫 u \cap Fin) X = ⋃ b)$
237	236	exlimdv	$⊢ (((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to (\exists f (f : t ⟶ 𝒫 u \cap Fin \land \forall s \in t X = ⋃ f (s) \cup s) \to \exists b \in (𝒫 u \cap Fin) X = ⋃ b)$
238	78 88 237	3syld	$⊢ (((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to (\forall s \in t \exists n \in (𝒫 (u \cup \{s\}) \cap Fin) X = ⋃ n \to \exists b \in (𝒫 u \cap Fin) X = ⋃ b)$
239	5 238	biimtrid	$⊢ (((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to (\neg \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n \to \exists b \in (𝒫 u \cap Fin) X = ⋃ b)$
240		dfrex2	$⊢ \exists b \in (𝒫 u \cap Fin) X = ⋃ b \leftrightarrow \neg \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b$
241	239 240	imbitrdi	$⊢ (((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to (\neg \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n \to \neg \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)$
242	241	con4d	$⊢ (((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \land w \in u)) \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)$
243	242	exp32	$⊢ ((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \to (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \to (w \in u \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)))$
244	243	com24	$⊢ ((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 (u \in 𝒫 fi (x) \land a \subseteq u)) \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to (w \in u \to (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \to \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)))$
245	244	exp32	$⊢ (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)) \to (u \in 𝒫 fi (x) \to (a \subseteq u \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to (w \in u \to (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \to \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)))))$
246	245	imp45	$⊢ ((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 (u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (w \in u \to (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \to \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))$
247	246	imp31	$⊢ ((((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 (u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \land w \in u) \land ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u)))) \to \exists s \in t \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n$

Metamath Proof Explorer

Theorem alexsubALTlem3

Proof