alexsubALTlem4

Description: Lemma for alexsubALT . If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010) (Revised by Mario Carneiro, 14-Dec-2013)

		Ref	Expression
	Hypothesis	alexsubALT.1	$⊢ X = ⋃ J$
	Assertion	alexsubALTlem4	$⊢ J = topGen (fi (x)) \to (\forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to \forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$

Proof

Step	Hyp	Ref	Expression
1		alexsubALT.1	$⊢ X = ⋃ J$
2		ralnex	$⊢ \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \leftrightarrow \neg \exists b \in (𝒫 a \cap Fin) X = ⋃ b$
3	1	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$
4		elun	$⊢ u \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \leftrightarrow (u \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \lor u \in \{\emptyset\})$
5		sseq2	$⊢ z = u \to (a \subseteq z \leftrightarrow a \subseteq u)$
6		pweq	$⊢ z = u \to 𝒫 z = 𝒫 u$
7	6	ineq1d	$⊢ z = u \to 𝒫 z \cap Fin = 𝒫 u \cap Fin$
8	7	raleqdv	$⊢ z = u \to (\forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b \leftrightarrow \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)$
9	5 8	anbi12d	$⊢ z = u \to ((a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b) \leftrightarrow (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))$
10	9	elrab	$⊢ u \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \leftrightarrow (u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))$
11		velsn	$⊢ u \in \{\emptyset\} \leftrightarrow u = \emptyset$
12	10 11	orbi12i	$⊢ (u \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \lor u \in \{\emptyset\}) \leftrightarrow ((u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)) \lor u = \emptyset)$
13	4 12	bitri	$⊢ u \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \leftrightarrow ((u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)) \lor u = \emptyset)$
14		ralnex	$⊢ \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 \leftrightarrow \neg \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v$
15		simprrl	$⊢ ((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 a \subseteq u$
16	15	unissd	$⊢ ((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 ⋃ a \subseteq ⋃ u$
17		sseq1	$⊢ X = ⋃ a \to (X \subseteq ⋃ u \leftrightarrow ⋃ a \subseteq ⋃ u)$
18	16 17	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (X = ⋃ a \to X \subseteq ⋃ u)$
19		vex	$⊢ x \in V$
20		inss1	$⊢ x \cap u \subseteq x$
21	19 20	elpwi2	$⊢ x \cap u \in 𝒫 x$
22		unieq	$⊢ c = x \cap u \to ⋃ c = ⋃ (x \cap u)$
23	22	eqeq2d	$⊢ c = x \cap u \to (X = ⋃ c \leftrightarrow X = ⋃ (x \cap u))$
24		pweq	$⊢ c = x \cap u \to 𝒫 c = 𝒫 (x \cap u)$
25	24	ineq1d	$⊢ c = x \cap u \to 𝒫 c \cap Fin = 𝒫 (x \cap u) \cap Fin$
26	25	rexeqdv	$⊢ c = x \cap u \to (\exists d \in (𝒫 c \cap Fin) X = ⋃ d \leftrightarrow \exists d \in (𝒫 (x \cap u) \cap Fin) X = ⋃ d)$
27	23 26	imbi12d	$⊢ c = x \cap u \to ((X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \leftrightarrow (X = ⋃ (x \cap u) \to \exists d \in (𝒫 (x \cap u) \cap Fin) X = ⋃ d))$
28	27	rspccv	$⊢ \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (x \cap u \in 𝒫 x \to (X = ⋃ (x \cap u) \to \exists d \in (𝒫 (x \cap u) \cap Fin) X = ⋃ d))$
29	21 28	mpi	$⊢ \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (X = ⋃ (x \cap u) \to \exists d \in (𝒫 (x \cap u) \cap Fin) X = ⋃ d)$
30		inss2	$⊢ x \cap u \subseteq u$
31		sstr	$⊢ (d \subseteq x \cap u \land x \cap u \subseteq u) \to d \subseteq u$
32	30 31	mpan2	$⊢ d \subseteq x \cap u \to d \subseteq u$
33	32	anim1i	$⊢ (d \subseteq x \cap u \land d \in Fin) \to (d \subseteq u \land d \in Fin)$
34		elfpw	$⊢ d \in (𝒫 (x \cap u) \cap Fin) \leftrightarrow (d \subseteq x \cap u \land d \in Fin)$
35		elfpw	$⊢ d \in (𝒫 u \cap Fin) \leftrightarrow (d \subseteq u \land d \in Fin)$
36	33 34 35	3imtr4i	$⊢ d \in (𝒫 (x \cap u) \cap Fin) \to d \in (𝒫 u \cap Fin)$
37	36	anim1i	$⊢ (d \in (𝒫 (x \cap u) \cap Fin) \land X = ⋃ d) \to (d \in (𝒫 u \cap Fin) \land X = ⋃ d)$
38	37	reximi2	$⊢ \exists d \in (𝒫 (x \cap u) \cap Fin) X = ⋃ d \to \exists d \in (𝒫 u \cap Fin) X = ⋃ d$
39	29 38	syl6	$⊢ \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (X = ⋃ (x \cap u) \to \exists d \in (𝒫 u \cap Fin) X = ⋃ d)$
40		unieq	$⊢ d = b \to ⋃ d = ⋃ b$
41	40	eqeq2d	$⊢ d = b \to (X = ⋃ d \leftrightarrow X = ⋃ b)$
42	41	cbvrexvw	$⊢ \exists d \in (𝒫 u \cap Fin) X = ⋃ d \leftrightarrow \exists b \in (𝒫 u \cap Fin) X = ⋃ b$
43	39 42	imbitrdi	$⊢ \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (X = ⋃ (x \cap u) \to \exists b \in (𝒫 u \cap Fin) X = ⋃ b)$
44		dfrex2	$⊢ \exists b \in (𝒫 u \cap Fin) X = ⋃ b \leftrightarrow \neg \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b$
45	43 44	imbitrdi	$⊢ \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (X = ⋃ (x \cap u) \to \neg \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)$
46	45	con2d	$⊢ \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to \neg X = ⋃ (x \cap u))$
47	46	a1d	$⊢ \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (a \subseteq u \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to \neg X = ⋃ (x \cap u)))$
48	47	3ad2ant2	$⊢ (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 (a \subseteq u \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to \neg X = ⋃ (x \cap u)))$
49	48	adantr	$⊢ ((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)) \to (a \subseteq u \to (\forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b \to \neg X = ⋃ (x \cap u)))$
50	49	impd	$⊢ ((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)) \to ((a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b) \to \neg X = ⋃ (x \cap u))$
51	50	impr	$⊢ ((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 \neg X = ⋃ (x \cap u)$
52	20	unissi	$⊢ ⋃ (x \cap u) \subseteq ⋃ x$
53		fiuni	$⊢ x \in V \to ⋃ x = ⋃ fi (x)$
54	53	elv	$⊢ ⋃ x = ⋃ fi (x)$
55		fibas	$⊢ fi (x) \in TopBases$
56		unitg	$⊢ fi (x) \in TopBases \to ⋃ topGen (fi (x)) = ⋃ fi (x)$
57	55 56	ax-mp	$⊢ ⋃ topGen (fi (x)) = ⋃ fi (x)$
58	54 57	eqtr4i	$⊢ ⋃ x = ⋃ topGen (fi (x))$
59		unieq	$⊢ J = topGen (fi (x)) \to ⋃ J = ⋃ topGen (fi (x))$
60	58 59	eqtr4id	$⊢ J = topGen (fi (x)) \to ⋃ x = ⋃ J$
61	60 1	eqtr4di	$⊢ J = topGen (fi (x)) \to ⋃ x = 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 ⋃ x = X$
63	62	adantr	$⊢ ((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 ⋃ x = X$
64	52 63	sseqtrid	$⊢ ((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 ⋃ (x \cap u) \subseteq X$
65		eqcom	$⊢ X = ⋃ (x \cap u) \leftrightarrow ⋃ (x \cap u) = X$
66		eqss	$⊢ ⋃ (x \cap u) = X \leftrightarrow (⋃ (x \cap u) \subseteq X \land X \subseteq ⋃ (x \cap u))$
67	66	baib	$⊢ ⋃ (x \cap u) \subseteq X \to (⋃ (x \cap u) = X \leftrightarrow X \subseteq ⋃ (x \cap u))$
68	65 67	bitrid	$⊢ ⋃ (x \cap u) \subseteq X \to (X = ⋃ (x \cap u) \leftrightarrow X \subseteq ⋃ (x \cap u))$
69	64 68	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (X = ⋃ (x \cap u) \leftrightarrow X \subseteq ⋃ (x \cap u))$
70	51 69	mtbid	$⊢ ((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 \neg X \subseteq ⋃ (x \cap u)$
71		sstr2	$⊢ X \subseteq ⋃ u \to (⋃ u \subseteq ⋃ (x \cap u) \to X \subseteq ⋃ (x \cap u))$
72	71	con3rr3	$⊢ \neg X \subseteq ⋃ (x \cap u) \to (X \subseteq ⋃ u \to \neg ⋃ u \subseteq ⋃ (x \cap u))$
73	70 72	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (X \subseteq ⋃ u \to \neg ⋃ u \subseteq ⋃ (x \cap u))$
74		nss	$⊢ \neg ⋃ u \subseteq ⋃ (x \cap u) \leftrightarrow \exists y (y \in ⋃ u \land \neg y \in ⋃ (x \cap u))$
75		df-rex	$⊢ \exists y \in ⋃ u \neg y \in ⋃ (x \cap u) \leftrightarrow \exists y (y \in ⋃ u \land \neg y \in ⋃ (x \cap u))$
76	74 75	bitr4i	$⊢ \neg ⋃ u \subseteq ⋃ (x \cap u) \leftrightarrow \exists y \in ⋃ u \neg y \in ⋃ (x \cap u)$
77		eluni2	$⊢ y \in ⋃ u \leftrightarrow \exists w \in u y \in w$
78		elpwi	$⊢ u \in 𝒫 fi (x) \to u \subseteq fi (x)$
79	78	sseld	$⊢ u \in 𝒫 fi (x) \to (w \in u \to w \in fi (x))$
80	79	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (w \in u \to w \in fi (x))$
81		elfi	$⊢ (w \in V \land x \in V) \to (w \in fi (x) \leftrightarrow \exists t \in (𝒫 x \cap Fin) w = ⋂ t)$
82	81	el2v	$⊢ w \in fi (x) \leftrightarrow \exists t \in (𝒫 x \cap Fin) w = ⋂ t$
83	80 82	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (w \in u \to \exists t \in (𝒫 x \cap Fin) w = ⋂ t)$
84	1	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$
85	78	adantr	$⊢ (u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)) \to u \subseteq fi (x)$
86	85	ad4antlr	$⊢ (((((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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to u \subseteq fi (x)$
87		ssfii	$⊢ x \in V \to x \subseteq fi (x)$
88	87	elv	$⊢ x \subseteq fi (x)$
89		elinel1	$⊢ t \in (𝒫 x \cap Fin) \to t \in 𝒫 x$
90	89	elpwid	$⊢ t \in (𝒫 x \cap Fin) \to t \subseteq x$
91	90	ad2antrr	$⊢ ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land (y \in w \land \neg y \in ⋃ (x \cap u))) \to t \subseteq x$
92	91	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to t \subseteq x$
93		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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to s \in t$
94	92 93	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to s \in x$
95	88 94	sselid	$⊢ (((((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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to s \in fi (x)$
96	95	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to \{s\} \subseteq fi (x)$
97	86 96	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to u \cup \{s\} \subseteq fi (x)$
98		fvex	$⊢ fi (x) \in V$
99	98	elpw2	$⊢ u \cup \{s\} \in 𝒫 fi (x) \leftrightarrow u \cup \{s\} \subseteq fi (x)$
100	97 99	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to u \cup \{s\} \in 𝒫 fi (x)$
101		simprl	$⊢ (u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)) \to a \subseteq u$
102	101	ad4antlr	$⊢ (((((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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to a \subseteq u$
103		ssun1	$⊢ u \subseteq u \cup \{s\}$
104	102 103	sstrdi	$⊢ (((((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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to a \subseteq u \cup \{s\}$
105		unieq	$⊢ n = b \to ⋃ n = ⋃ b$
106	105	eqeq2d	$⊢ n = b \to (X = ⋃ n \leftrightarrow X = ⋃ b)$
107	106	notbid	$⊢ n = b \to (\neg X = ⋃ n \leftrightarrow \neg X = ⋃ b)$
108	107	cbvralvw	$⊢ \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n \leftrightarrow \forall b \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ b$
109	108	biimpi	$⊢ \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n \to \forall b \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ b$
110	109	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to \forall b \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ b$
111	100 104 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 (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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to (u \cup \{s\} \in 𝒫 fi (x) \land (a \subseteq u \cup \{s\} \land \forall b \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ b))$
112		sseq2	$⊢ z = u \cup \{s\} \to (a \subseteq z \leftrightarrow a \subseteq u \cup \{s\})$
113		pweq	$⊢ z = u \cup \{s\} \to 𝒫 z = 𝒫 (u \cup \{s\})$
114	113	ineq1d	$⊢ z = u \cup \{s\} \to 𝒫 z \cap Fin = 𝒫 (u \cup \{s\}) \cap Fin$
115	114	raleqdv	$⊢ z = u \cup \{s\} \to (\forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b \leftrightarrow \forall b \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ b)$
116	112 115	anbi12d	$⊢ z = u \cup \{s\} \to ((a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b) \leftrightarrow (a \subseteq u \cup \{s\} \land \forall b \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ b))$
117	116	elrab	$⊢ u \cup \{s\} \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \leftrightarrow (u \cup \{s\} \in 𝒫 fi (x) \land (a \subseteq u \cup \{s\} \land \forall b \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ b))$
118	111 117	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to u \cup \{s\} \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}$
119		elun1	$⊢ u \cup \{s\} \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \to u \cup \{s\} \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\})$
120	118 119	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to u \cup \{s\} \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\})$
121		vsnid	$⊢ s \in \{s\}$
122		elun2	$⊢ s \in \{s\} \to s \in (u \cup \{s\})$
123	121 122	ax-mp	$⊢ s \in (u \cup \{s\})$
124		intss1	$⊢ s \in t \to ⋂ t \subseteq s$
125		sseq1	$⊢ w = ⋂ t \to (w \subseteq s \leftrightarrow ⋂ t \subseteq s)$
126	124 125	syl5ibrcom	$⊢ s \in t \to (w = ⋂ t \to w \subseteq s)$
127	126	impcom	$⊢ (w = ⋂ t \land s \in t) \to w \subseteq s$
128	127	ad4ant24	$⊢ (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land y \in w) \land s \in t) \to w \subseteq s$
129	128	adantl	$⊢ (w \in u \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land y \in w) \land s \in t)) \to w \subseteq s$
130	129	adantrrr	$⊢ (w \in u \land (((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land y \in w) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to w \subseteq s$
131	130	adantll	$⊢ ((((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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to w \subseteq s$
132		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 (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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to y \in w$
133	131 132	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 \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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to y \in s$
134	90	ad2antrr	$⊢ ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \land y \in w) \to t \subseteq x$
135	134	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 \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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to t \subseteq x$
136		simprrl	$⊢ ((((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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to s \in t$
137	135 136	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 \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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to s \in x$
138		elin	$⊢ s \in (x \cap u) \leftrightarrow (s \in x \land s \in u)$
139		elunii	$⊢ (y \in s \land s \in (x \cap u)) \to y \in ⋃ (x \cap u)$
140	139	ex	$⊢ y \in s \to (s \in (x \cap u) \to y \in ⋃ (x \cap u))$
141	138 140	biimtrrid	$⊢ y \in s \to ((s \in x \land s \in u) \to y \in ⋃ (x \cap u))$
142	141	expd	$⊢ y \in s \to (s \in x \to (s \in u \to y \in ⋃ (x \cap u)))$
143	133 137 142	sylc	$⊢ ((((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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to (s \in u \to y \in ⋃ (x \cap u))$
144	143	con3d	$⊢ ((((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 (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n))) \to (\neg y \in ⋃ (x \cap u) \to \neg s \in u)$
145	144	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 \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)) \to ((s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n) \to (\neg y \in ⋃ (x \cap u) \to \neg s \in u))$
146	145	com23	$⊢ ((((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)) \to (\neg y \in ⋃ (x \cap u) \to ((s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n) \to \neg s \in u))$
147	146	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 \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \land w \in u) \to ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \to (y \in w \to (\neg y \in ⋃ (x \cap u) \to ((s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n) \to \neg s \in u))))$
148	147	imp55	$⊢ (((((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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to \neg s \in u$
149		vex	$⊢ s \in V$
150		eleq1w	$⊢ v = s \to (v \in (u \cup \{s\}) \leftrightarrow s \in (u \cup \{s\}))$
151		elequ1	$⊢ v = s \to (v \in u \leftrightarrow s \in u)$
152	151	notbid	$⊢ v = s \to (\neg v \in u \leftrightarrow \neg s \in u)$
153	150 152	anbi12d	$⊢ v = s \to ((v \in (u \cup \{s\}) \land \neg v \in u) \leftrightarrow (s \in (u \cup \{s\}) \land \neg s \in u))$
154	149 153	spcev	$⊢ (s \in (u \cup \{s\}) \land \neg s \in u) \to \exists v (v \in (u \cup \{s\}) \land \neg v \in u)$
155	123 148 154	sylancr	$⊢ (((((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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to \exists v (v \in (u \cup \{s\}) \land \neg v \in u)$
156		nss	$⊢ \neg u \cup \{s\} \subseteq u \leftrightarrow \exists v (v \in (u \cup \{s\}) \land \neg v \in u)$
157	155 156	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to \neg u \cup \{s\} \subseteq u$
158		eqimss2	$⊢ u = u \cup \{s\} \to u \cup \{s\} \subseteq u$
159	158	necon3bi	$⊢ \neg u \cup \{s\} \subseteq u \to u \neq u \cup \{s\}$
160	157 159	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to u \neq u \cup \{s\}$
161	160 103	jctil	$⊢ (((((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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to (u \subseteq u \cup \{s\} \land u \neq u \cup \{s\})$
162		df-pss	$⊢ u \subset u \cup \{s\} \leftrightarrow (u \subseteq u \cup \{s\} \land u \neq u \cup \{s\})$
163	161 162	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to u \subset u \cup \{s\}$
164		psseq2	$⊢ v = u \cup \{s\} \to (u \subset v \leftrightarrow u \subset u \cup \{s\})$
165	164	rspcev	$⊢ (u \cup \{s\} \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \land u \subset u \cup \{s\}) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v$
166	120 163 165	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 \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)))) \land (s \in t \land \forall n \in (𝒫 (u \cup \{s\}) \cap Fin) \neg X = ⋃ n)) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v$
167	84 166	rexlimddv	$⊢ ((((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 v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v$
168	167	exp45	$⊢ (((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) \to ((t \in (𝒫 x \cap Fin) \land w = ⋂ t) \to (y \in w \to (\neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v)))$
169	168	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \land w \in u) \to (t \in (𝒫 x \cap Fin) \to (w = ⋂ t \to (y \in w \to (\neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v))))$
170	169	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \land w \in u) \to (\exists t \in (𝒫 x \cap Fin) w = ⋂ t \to (y \in w \to (\neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v)))$
171	170	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (w \in u \to (\exists t \in (𝒫 x \cap Fin) w = ⋂ t \to (y \in w \to (\neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v))))$
172	83 171	mpdd	$⊢ ((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 (y \in w \to (\neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v)))$
173	172	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (\exists w \in u y \in w \to (\neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v))$
174	77 173	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (y \in ⋃ u \to (\neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v))$
175	174	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (\exists y \in ⋃ u \neg y \in ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v)$
176	76 175	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (\neg ⋃ u \subseteq ⋃ (x \cap u) \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v)$
177	18 73 176	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (X = ⋃ a \to \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v)$
178	177	con3d	$⊢ ((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 (\neg \exists v \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) u \subset v \to \neg X = ⋃ a)$
179	14 178	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 \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b))) \to (\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 \to \neg X = ⋃ a)$
180	179	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)) \to ((u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)) \to (\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 \to \neg X = ⋃ a))$
181	180	adantr	$⊢ ((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 ((u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)) \to (\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 \to \neg X = ⋃ a))$
182		ssun1	$⊢ \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \subseteq \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}$
183		eqimss2	$⊢ z = a \to a \subseteq z$
184	183	biantrurd	$⊢ z = a \to (\forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b \leftrightarrow (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b))$
185		pweq	$⊢ z = a \to 𝒫 z = 𝒫 a$
186	185	ineq1d	$⊢ z = a \to 𝒫 z \cap Fin = 𝒫 a \cap Fin$
187	186	raleqdv	$⊢ z = a \to (\forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b \leftrightarrow \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b)$
188	184 187	bitr3d	$⊢ z = a \to ((a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b) \leftrightarrow \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b)$
189		simpll3	$⊢ (((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 u = \emptyset) \to a \in 𝒫 fi (x)$
190		simplr	$⊢ (((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 u = \emptyset) \to \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b$
191	188 189 190	elrabd	$⊢ (((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 u = \emptyset) \to a \in \{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\}$
192	182 191	sselid	$⊢ (((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 u = \emptyset) \to a \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\})$
193		psseq2	$⊢ v = a \to (u \subset v \leftrightarrow u \subset a)$
194	193	notbid	$⊢ v = a \to (\neg u \subset v \leftrightarrow \neg u \subset a)$
195	194	rspcv	$⊢ a \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \to (\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 \to \neg u \subset a)$
196	192 195	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) \land u = \emptyset) \to (\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 \to \neg u \subset a)$
197		id	$⊢ a = \emptyset \to a = \emptyset$
198		0elpw	$⊢ \emptyset \in 𝒫 a$
199		0fi	$⊢ \emptyset \in Fin$
200	198 199	elini	$⊢ \emptyset \in (𝒫 a \cap Fin)$
201	197 200	eqeltrdi	$⊢ a = \emptyset \to a \in (𝒫 a \cap Fin)$
202		unieq	$⊢ b = a \to ⋃ b = ⋃ a$
203	202	eqeq2d	$⊢ b = a \to (X = ⋃ b \leftrightarrow X = ⋃ a)$
204	203	notbid	$⊢ b = a \to (\neg X = ⋃ b \leftrightarrow \neg X = ⋃ a)$
205	204	rspccv	$⊢ \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \to (a \in (𝒫 a \cap Fin) \to \neg X = ⋃ a)$
206	201 205	syl5	$⊢ \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \to (a = \emptyset \to \neg X = ⋃ a)$
207	206	necon2ad	$⊢ \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \to (X = ⋃ a \to a \neq \emptyset)$
208	207	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 u = \emptyset) \to (X = ⋃ a \to a \neq \emptyset)$
209		psseq1	$⊢ u = \emptyset \to (u \subset a \leftrightarrow \emptyset \subset a)$
210	209	adantl	$⊢ (((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 u = \emptyset) \to (u \subset a \leftrightarrow \emptyset \subset a)$
211		0pss	$⊢ \emptyset \subset a \leftrightarrow a \neq \emptyset$
212	210 211	bitrdi	$⊢ (((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 u = \emptyset) \to (u \subset a \leftrightarrow a \neq \emptyset)$
213	208 212	sylibrd	$⊢ (((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 u = \emptyset) \to (X = ⋃ a \to u \subset a)$
214	196 213	nsyld	$⊢ (((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 u = \emptyset) \to (\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 \to \neg X = ⋃ a)$
215	214	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 (u = \emptyset \to (\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 \to \neg X = ⋃ a))$
216	181 215	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 \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \to (((u \in 𝒫 fi (x) \land (a \subseteq u \land \forall b \in (𝒫 u \cap Fin) \neg X = ⋃ b)) \lor u = \emptyset) \to (\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 \to \neg X = ⋃ a))$
217	13 216	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 \forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b) \to (u \in (\{z \in 𝒫 fi (x) \| (a \subseteq z \land \forall b \in (𝒫 z \cap Fin) \neg X = ⋃ b)\} \cup \{\emptyset\}) \to (\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 \to \neg X = ⋃ a))$
218	217	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) \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 \to \neg X = ⋃ a)$
219	3 218	mpd	$⊢ ((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 \neg X = ⋃ a$
220	219	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)) \to (\forall b \in (𝒫 a \cap Fin) \neg X = ⋃ b \to \neg X = ⋃ a)$
221	2 220	biimtrrid	$⊢ (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 (\neg \exists b \in (𝒫 a \cap Fin) X = ⋃ b \to \neg X = ⋃ a)$
222	221	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)) \to (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
223	222	3exp	$⊢ J = topGen (fi (x)) \to (\forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to (a \in 𝒫 fi (x) \to (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)))$
224	223	ralrimdv	$⊢ J = topGen (fi (x)) \to (\forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to \forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$

Metamath Proof Explorer

Theorem alexsubALTlem4

Proof