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		vex	$⊢ s \in V$
39	38	unisn	$⊢ ⋃ \{s\} = s$
40	39	uneq2i	$⊢ ⋃ (n ∖ \{s\}) \cup ⋃ \{s\} = ⋃ (n ∖ \{s\}) \cup s$
41	37 40	eqtri	$⊢ ⋃ ((n ∖ \{s\}) \cup \{s\}) = ⋃ (n ∖ \{s\}) \cup s$
42	36 41	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$
43	25 42	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$
44		difss	$⊢ n ∖ \{s\} \subseteq n$
45	44	unissi	$⊢ ⋃ (n ∖ \{s\}) \subseteq ⋃ n$
46		sseq2	$⊢ X = ⋃ n \to (⋃ (n ∖ \{s\}) \subseteq X \leftrightarrow ⋃ (n ∖ \{s\}) \subseteq ⋃ n)$
47	45 46	mpbiri	$⊢ X = ⋃ n \to ⋃ (n ∖ \{s\}) \subseteq X$
48	47	adantl	$⊢ (n \in (𝒫 (u \cup \{s\}) \cap Fin) \land X = ⋃ n) \to ⋃ (n ∖ \{s\}) \subseteq X$
49	48	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$
50		elinel1	$⊢ t \in (𝒫 x \cap Fin) \to t \in 𝒫 x$
51	50	elpwid	$⊢ t \in (𝒫 x \cap Fin) \to t \subseteq x$
52	51	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$
53	52	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$
54		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$
55	53 54	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$
56		elssuni	$⊢ s \in x \to s \subseteq ⋃ x$
57	55 56	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$
58		fibas	$⊢ fi (x) \in TopBases$
59		unitg	$⊢ fi (x) \in TopBases \to ⋃ topGen (fi (x)) = ⋃ fi (x)$
60	58 59	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)$
61		unieq	$⊢ J = topGen (fi (x)) \to ⋃ J = ⋃ topGen (fi (x))$
62	61	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))$
63	62	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))$
64		vex	$⊢ x \in V$
65		fiuni	$⊢ x \in V \to ⋃ x = ⋃ fi (x)$
66	64 65	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)$
67	60 63 66	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$
68	67 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$
69	57 68	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$
70	49 69	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$
71	43 70	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$
72		unieq	$⊢ m = n ∖ \{s\} \to ⋃ m = ⋃ (n ∖ \{s\})$
73	72	uneq1d	$⊢ m = n ∖ \{s\} \to ⋃ m \cup s = ⋃ (n ∖ \{s\}) \cup s$
74	73	rspceeqv	$⊢ (n ∖ \{s\} \in (𝒫 u \cap Fin) \land X = ⋃ (n ∖ \{s\}) \cup s) \to \exists m \in (𝒫 u \cap Fin) X = ⋃ m \cup s$
75	24 71 74	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$
76	75	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)$
77	76	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))$
78	77	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)$
79	78	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)$
80		elinel2	$⊢ t \in (𝒫 x \cap Fin) \to t \in Fin$
81	80	adantr	$⊢ (t \in (𝒫 x \cap Fin) \land w = ⋂ t) \to t \in Fin$
82		unieq	$⊢ m = f (s) \to ⋃ m = ⋃ f (s)$
83	82	uneq1d	$⊢ m = f (s) \to ⋃ m \cup s = ⋃ f (s) \cup s$
84	83	eqeq2d	$⊢ m = f (s) \to (X = ⋃ m \cup s \leftrightarrow X = ⋃ f (s) \cup s)$
85	84	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)$
86	85	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))$
87	81 86	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))$
88	87	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))$
89	88	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))$
90		ffvelrn	$⊢ (f : t ⟶ 𝒫 u \cap Fin \land s \in t) \to f (s) \in (𝒫 u \cap Fin)$
91		elin	$⊢ f (s) \in (𝒫 u \cap Fin) \leftrightarrow (f (s) \in 𝒫 u \land f (s) \in Fin)$
92		elpwi	$⊢ f (s) \in 𝒫 u \to f (s) \subseteq u$
93	92	adantr	$⊢ (f (s) \in 𝒫 u \land f (s) \in Fin) \to f (s) \subseteq u$
94	91 93	sylbi	$⊢ f (s) \in (𝒫 u \cap Fin) \to f (s) \subseteq u$
95	90 94	syl	$⊢ (f : t ⟶ 𝒫 u \cap Fin \land s \in t) \to f (s) \subseteq u$
96	95	ralrimiva	$⊢ f : t ⟶ 𝒫 u \cap Fin \to \forall s \in t f (s) \subseteq u$
97		iunss	$⊢ ⋃_{s \in t} f (s) \subseteq u \leftrightarrow \forall s \in t f (s) \subseteq u$
98	96 97	sylibr	$⊢ f : t ⟶ 𝒫 u \cap Fin \to ⋃_{s \in t} f (s) \subseteq u$
99	98	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$
100		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$
101	100	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$
102	99 101	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$
103	90	elin2d	$⊢ (f : t ⟶ 𝒫 u \cap Fin \land s \in t) \to f (s) \in Fin$
104	103	ralrimiva	$⊢ f : t ⟶ 𝒫 u \cap Fin \to \forall s \in t f (s) \in Fin$
105		iunfi	$⊢ (t \in Fin \land \forall s \in t f (s) \in Fin) \to ⋃_{s \in t} f (s) \in Fin$
106	81 104 105	syl2an	$⊢ ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land f : t ⟶ 𝒫 u \cap Fin) \to ⋃_{s \in t} f (s) \in Fin$
107	106	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$
108	107	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$
109		snfi	$⊢ \{w\} \in Fin$
110		unfi	$⊢ (⋃_{s \in t} f (s) \in Fin \land \{w\} \in Fin) \to ⋃_{s \in t} f (s) \cup \{w\} \in Fin$
111	108 109 110	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$
112	102 111	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)$
113		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)$
114	20	elpw2	$⊢ ⋃_{s \in t} f (s) \cup \{w\} \in 𝒫 u \leftrightarrow ⋃_{s \in t} f (s) \cup \{w\} \subseteq u$
115	114	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)$
116	113 115	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)$
117	112 116	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)$
118		ralnex	$⊢ \forall s \in t \neg y \in f (s) \leftrightarrow \neg \exists s \in t y \in f (s)$
119	118	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))$
120	119	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))$
121		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))$
122	120 121	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))$
123		fveq2	$⊢ s = z \to f (s) = f (z)$
124	123	unieqd	$⊢ s = z \to ⋃ f (s) = ⋃ f (z)$
125		id	$⊢ s = z \to s = z$
126	124 125	uneq12d	$⊢ s = z \to ⋃ f (s) \cup s = ⋃ f (z) \cup z$
127	126	eqeq2d	$⊢ s = z \to (X = ⋃ f (s) \cup s \leftrightarrow X = ⋃ f (z) \cup z)$
128	127	rspcv	$⊢ z \in t \to (\forall s \in t X = ⋃ f (s) \cup s \to X = ⋃ f (z) \cup z)$
129		eleq2	$⊢ X = ⋃ f (z) \cup z \to (v \in X \leftrightarrow v \in (⋃ f (z) \cup z))$
130	129	biimpd	$⊢ X = ⋃ f (z) \cup z \to (v \in X \to v \in (⋃ f (z) \cup z))$
131		elun	$⊢ v \in (⋃ f (z) \cup z) \leftrightarrow (v \in ⋃ f (z) \lor v \in z)$
132		eluni	$⊢ v \in ⋃ f (z) \leftrightarrow \exists w (v \in w \land w \in f (z))$
133	132	orbi1i	$⊢ (v \in ⋃ f (z) \lor v \in z) \leftrightarrow (\exists w (v \in w \land w \in f (z)) \lor v \in z)$
134		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)$
135		alinexa	$⊢ \forall w (v \in w \to \neg w \in f (z)) \leftrightarrow \neg \exists w (v \in w \land w \in f (z))$
136	135	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)$
137	134 136	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)$
138	131 133 137	3bitri	$⊢ v \in (⋃ f (z) \cup z) \leftrightarrow (\forall w (v \in w \to \neg w \in f (z)) \to v \in z)$
139		eleq2	$⊢ y = w \to (v \in y \leftrightarrow v \in w)$
140		eleq1w	$⊢ y = w \to (y \in f (s) \leftrightarrow w \in f (s))$
141	140	notbid	$⊢ y = w \to (\neg y \in f (s) \leftrightarrow \neg w \in f (s))$
142	141	ralbidv	$⊢ y = w \to (\forall s \in t \neg y \in f (s) \leftrightarrow \forall s \in t \neg w \in f (s))$
143	139 142	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)))$
144	143	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))$
145	123	eleq2d	$⊢ s = z \to (w \in f (s) \leftrightarrow w \in f (z))$
146	145	notbid	$⊢ s = z \to (\neg w \in f (s) \leftrightarrow \neg w \in f (z))$
147	146	rspcv	$⊢ z \in t \to (\forall s \in t \neg w \in f (s) \to \neg w \in f (z))$
148	144 147	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)))$
149	148	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)))$
150	149	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))$
151	138 150	syl5bi	$⊢ 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))$
152	151	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)))$
153	130 152	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))))$
154	128 153	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))))$
155	154	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))))$
156	155	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))$
157	156	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))$
158	157	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)$
159		vex	$⊢ v \in V$
160	159	elint2	$⊢ v \in ⋂ t \leftrightarrow \forall z \in t v \in z$
161	158 160	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)$
162		eleq2	$⊢ w = ⋂ t \to (v \in w \leftrightarrow v \in ⋂ t)$
163	162	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)$
164	161 163	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)$
165	122 164	syl5bi	$⊢ ((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)$
166	165	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)$
167	166	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))$
168		orc	$⊢ \exists s \in t y \in f (s) \to (\exists s \in t y \in f (s) \lor y = w)$
169	168	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))$
170	169	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))$
171		equid	$⊢ w = w$
172		vex	$⊢ w \in V$
173		equequ1	$⊢ y = w \to (y = w \leftrightarrow w = w)$
174	139 173	anbi12d	$⊢ y = w \to ((v \in y \land y = w) \leftrightarrow (v \in w \land w = w))$
175	172 174	spcev	$⊢ (v \in w \land w = w) \to \exists y (v \in y \land y = w)$
176	171 175	mpan2	$⊢ v \in w \to \exists y (v \in y \land y = w)$
177		olc	$⊢ y = w \to (\exists s \in t y \in f (s) \lor y = w)$
178	177	anim2i	$⊢ (v \in y \land y = w) \to (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
179	178	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))$
180	176 179	syl	$⊢ v \in w \to \exists y (v \in y \land (\exists s \in t y \in f (s) \lor y = w))$
181	170 180	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))$
182		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\}))$
183		elun	$⊢ y \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (y \in ⋃_{s \in t} f (s) \lor y \in \{w\})$
184		eliun	$⊢ y \in ⋃_{s \in t} f (s) \leftrightarrow \exists s \in t y \in f (s)$
185		velsn	$⊢ y \in \{w\} \leftrightarrow y = w$
186	184 185	orbi12i	$⊢ (y \in ⋃_{s \in t} f (s) \lor y \in \{w\}) \leftrightarrow (\exists s \in t y \in f (s) \lor y = w)$
187	183 186	bitri	$⊢ y \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (\exists s \in t y \in f (s) \lor y = w)$
188	187	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))$
189	188	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))$
190	182 189	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\})$
191	181 190	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\})$
192	167 191	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\}))$
193	192	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\}))$
194	193	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\}))$
195	194	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\})$
196		elun	$⊢ v \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (v \in ⋃_{s \in t} f (s) \lor v \in \{w\})$
197		eliun	$⊢ v \in ⋃_{s \in t} f (s) \leftrightarrow \exists s \in t v \in f (s)$
198		velsn	$⊢ v \in \{w\} \leftrightarrow v = w$
199	197 198	orbi12i	$⊢ (v \in ⋃_{s \in t} f (s) \lor v \in \{w\}) \leftrightarrow (\exists s \in t v \in f (s) \lor v = w)$
200	196 199	bitri	$⊢ v \in (⋃_{s \in t} f (s) \cup \{w\}) \leftrightarrow (\exists s \in t v \in f (s) \lor v = w)$
201		nfra1	$⊢ Ⅎ s \forall s \in t X = ⋃ f (s) \cup s$
202		nfv	$⊢ Ⅎ s v \subseteq X$
203		rsp	$⊢ \forall s \in t X = ⋃ f (s) \cup s \to (s \in t \to X = ⋃ f (s) \cup s)$
204		eqimss2	$⊢ X = ⋃ f (s) \cup s \to ⋃ f (s) \cup s \subseteq X$
205		elssuni	$⊢ v \in f (s) \to v \subseteq ⋃ f (s)$
206		ssun3	$⊢ v \subseteq ⋃ f (s) \to v \subseteq ⋃ f (s) \cup s$
207	205 206	syl	$⊢ v \in f (s) \to v \subseteq ⋃ f (s) \cup s$
208		sstr	$⊢ (v \subseteq ⋃ f (s) \cup s \land ⋃ f (s) \cup s \subseteq X) \to v \subseteq X$
209	208	expcom	$⊢ ⋃ f (s) \cup s \subseteq X \to (v \subseteq ⋃ f (s) \cup s \to v \subseteq X)$
210	204 207 209	syl2im	$⊢ X = ⋃ f (s) \cup s \to (v \in f (s) \to v \subseteq X)$
211	203 210	syl6	$⊢ \forall s \in t X = ⋃ f (s) \cup s \to (s \in t \to (v \in f (s) \to v \subseteq X))$
212	201 202 211	rexlimd	$⊢ \forall s \in t X = ⋃ f (s) \cup s \to (\exists s \in t v \in f (s) \to v \subseteq X)$
213	212	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)$
214		elpwi	$⊢ u \in 𝒫 fi (x) \to u \subseteq fi (x)$
215	214	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)$
216	215	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)$
217	216 100	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)$
218		elssuni	$⊢ w \in fi (x) \to w \subseteq ⋃ fi (x)$
219	217 218	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)$
220	58 59	ax-mp	$⊢ ⋃ topGen (fi (x)) = ⋃ fi (x)$
221	61 220	eqtr2di	$⊢ J = topGen (fi (x)) \to ⋃ fi (x) = ⋃ J$
222	221 1	eqtr4di	$⊢ J = topGen (fi (x)) \to ⋃ fi (x) = X$
223	222	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$
224	223	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$
225	219 224	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$
226		sseq1	$⊢ v = w \to (v \subseteq X \leftrightarrow w \subseteq X)$
227	225 226	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)$
228	213 227	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)$
229	200 228	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 (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)$
230	229	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$
231		unissb	$⊢ ⋃ (⋃_{s \in t} f (s) \cup \{w\}) \subseteq X \leftrightarrow \forall v \in (⋃_{s \in t} f (s) \cup \{w\}) v \subseteq X$
232	230 231	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$
233	195 232	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\})$
234		unieq	$⊢ b = ⋃_{s \in t} f (s) \cup \{w\} \to ⋃ b = ⋃ (⋃_{s \in t} f (s) \cup \{w\})$
235	234	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$
236	117 233 235	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$
237	236	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)$
238	237	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)$
239	79 89 238	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)$
240	5 239	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 (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)$
241		dfrex2	$⊢ \exists b \in (𝒫 u \cap Fin) X = ⋃ b \leftrightarrow \neg \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b$
242	240 241	syl6ib	$⊢ (((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)$
243	242	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)$
244	243	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)))$
245	244	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)))$
246	245	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)))))$
247	246	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))$
248	247	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