2ndcctbss

Description: If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010) (Proof shortened by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Hypotheses	2ndcctbss.1	$⊢ J = topGen (B)$
	2ndcctbss.2	$⊢ S = \{⟨u, v⟩ \| (u \in c \land v \in c \land \exists w \in B (u \subseteq w \land w \subseteq v))\}$
Assertion	2ndcctbss	$⊢ (B \in TopBases \land J \in 2^{nd} 𝜔) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b))$

Proof

Step	Hyp	Ref	Expression
1		2ndcctbss.1	$⊢ J = topGen (B)$
2		2ndcctbss.2	$⊢ S = \{⟨u, v⟩ \| (u \in c \land v \in c \land \exists w \in B (u \subseteq w \land w \subseteq v))\}$
3		simpr	$⊢ (B \in TopBases \land J \in 2^{nd} 𝜔) \to J \in 2^{nd} 𝜔$
4		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists c \in TopBases (c ≼ ω \land topGen (c) = J)$
5	3 4	sylib	$⊢ (B \in TopBases \land J \in 2^{nd} 𝜔) \to \exists c \in TopBases (c ≼ ω \land topGen (c) = J)$
6		vex	$⊢ c \in V$
7	6 6	xpex	$⊢ c \times c \in V$
8		3simpa	$⊢ (u \in c \land v \in c \land \exists w \in B (u \subseteq w \land w \subseteq v)) \to (u \in c \land v \in c)$
9	8	ssopab2i	$⊢ \{⟨u, v⟩ \| (u \in c \land v \in c \land \exists w \in B (u \subseteq w \land w \subseteq v))\} \subseteq \{⟨u, v⟩ \| (u \in c \land v \in c)\}$
10		df-xp	$⊢ c \times c = \{⟨u, v⟩ \| (u \in c \land v \in c)\}$
11	9 2 10	3sstr4i	$⊢ S \subseteq c \times c$
12		ssdomg	$⊢ c \times c \in V \to (S \subseteq c \times c \to S ≼ (c \times c))$
13	7 11 12	mp2	$⊢ S ≼ (c \times c)$
14	6	xpdom1	$⊢ c ≼ ω \to (c \times c) ≼ (ω \times c)$
15		omex	$⊢ ω \in V$
16	15	xpdom2	$⊢ c ≼ ω \to (ω \times c) ≼ (ω \times ω)$
17		domtr	$⊢ ((c \times c) ≼ (ω \times c) \land (ω \times c) ≼ (ω \times ω)) \to (c \times c) ≼ (ω \times ω)$
18	14 16 17	syl2anc	$⊢ c ≼ ω \to (c \times c) ≼ (ω \times ω)$
19		xpomen	$⊢ (ω \times ω) \approx ω$
20		domentr	$⊢ ((c \times c) ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to (c \times c) ≼ ω$
21	18 19 20	sylancl	$⊢ c ≼ ω \to (c \times c) ≼ ω$
22	21	adantr	$⊢ (c ≼ ω \land topGen (c) = J) \to (c \times c) ≼ ω$
23	22	ad2antll	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to (c \times c) ≼ ω$
24		domtr	$⊢ (S ≼ (c \times c) \land (c \times c) ≼ ω) \to S ≼ ω$
25	13 23 24	sylancr	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to S ≼ ω$
26	2	relopabiv	$⊢ Rel S$
27		simpr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land x \in S) \to x \in S$
28		1st2nd	$⊢ (Rel S \land x \in S) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
29	26 27 28	sylancr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land x \in S) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
30	29 27	eqeltrrd	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land x \in S) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in S$
31		df-br	$⊢ 1^{st} (x) S 2^{nd} (x) \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ \in S$
32		fvex	$⊢ 1^{st} (x) \in V$
33		fvex	$⊢ 2^{nd} (x) \in V$
34		simpl	$⊢ (u = 1^{st} (x) \land v = 2^{nd} (x)) \to u = 1^{st} (x)$
35	34	eleq1d	$⊢ (u = 1^{st} (x) \land v = 2^{nd} (x)) \to (u \in c \leftrightarrow 1^{st} (x) \in c)$
36		simpr	$⊢ (u = 1^{st} (x) \land v = 2^{nd} (x)) \to v = 2^{nd} (x)$
37	36	eleq1d	$⊢ (u = 1^{st} (x) \land v = 2^{nd} (x)) \to (v \in c \leftrightarrow 2^{nd} (x) \in c)$
38		sseq1	$⊢ u = 1^{st} (x) \to (u \subseteq w \leftrightarrow 1^{st} (x) \subseteq w)$
39		sseq2	$⊢ v = 2^{nd} (x) \to (w \subseteq v \leftrightarrow w \subseteq 2^{nd} (x))$
40	38 39	bi2anan9	$⊢ (u = 1^{st} (x) \land v = 2^{nd} (x)) \to ((u \subseteq w \land w \subseteq v) \leftrightarrow (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x)))$
41	40	rexbidv	$⊢ (u = 1^{st} (x) \land v = 2^{nd} (x)) \to (\exists w \in B (u \subseteq w \land w \subseteq v) \leftrightarrow \exists w \in B (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x)))$
42	35 37 41	3anbi123d	$⊢ (u = 1^{st} (x) \land v = 2^{nd} (x)) \to ((u \in c \land v \in c \land \exists w \in B (u \subseteq w \land w \subseteq v)) \leftrightarrow (1^{st} (x) \in c \land 2^{nd} (x) \in c \land \exists w \in B (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x))))$
43	32 33 42 2	braba	$⊢ 1^{st} (x) S 2^{nd} (x) \leftrightarrow (1^{st} (x) \in c \land 2^{nd} (x) \in c \land \exists w \in B (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x)))$
44	31 43	bitr3i	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in S \leftrightarrow (1^{st} (x) \in c \land 2^{nd} (x) \in c \land \exists w \in B (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x)))$
45	44	simp3bi	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in S \to \exists w \in B (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x))$
46	30 45	syl	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land x \in S) \to \exists w \in B (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x))$
47		fvi	$⊢ B \in TopBases \to I (B) = B$
48	47	ad3antrrr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land x \in S) \to I (B) = B$
49	46 48	rexeqtrrdv	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land x \in S) \to \exists w \in I (B) (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x))$
50	49	ralrimiva	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to \forall x \in S \exists w \in I (B) (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x))$
51		fvex	$⊢ I (B) \in V$
52		sseq2	$⊢ w = f (x) \to (1^{st} (x) \subseteq w \leftrightarrow 1^{st} (x) \subseteq f (x))$
53		sseq1	$⊢ w = f (x) \to (w \subseteq 2^{nd} (x) \leftrightarrow f (x) \subseteq 2^{nd} (x))$
54	52 53	anbi12d	$⊢ w = f (x) \to ((1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x)) \leftrightarrow (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))$
55	51 54	axcc4dom	$⊢ (S ≼ ω \land \forall x \in S \exists w \in I (B) (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x))) \to \exists f (f : S ⟶ I (B) \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))$
56	25 50 55	syl2anc	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to \exists f (f : S ⟶ I (B) \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))$
57	47	ad2antrr	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to I (B) = B$
58	57	feq3d	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to (f : S ⟶ I (B) \leftrightarrow f : S ⟶ B)$
59	58	anbi1d	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to ((f : S ⟶ I (B) \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \leftrightarrow (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))))$
60		2ndctop	$⊢ J \in 2^{nd} 𝜔 \to J \in Top$
61	60	adantl	$⊢ (B \in TopBases \land J \in 2^{nd} 𝜔) \to J \in Top$
62	61	ad2antrr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to J \in Top$
63		frn	$⊢ f : S ⟶ B \to ran f \subseteq B$
64	63	ad2antrl	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to ran f \subseteq B$
65		bastg	$⊢ B \in TopBases \to B \subseteq topGen (B)$
66	65	ad3antrrr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to B \subseteq topGen (B)$
67	66 1	sseqtrrdi	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to B \subseteq J$
68	64 67	sstrd	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to ran f \subseteq J$
69		simprrl	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to o \in J$
70		simprr	$⊢ (c \in TopBases \land (c ≼ ω \land topGen (c) = J)) \to topGen (c) = J$
71	70	ad2antlr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to topGen (c) = J$
72	69 71	eleqtrrd	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to o \in topGen (c)$
73		simprrr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to t \in o$
74		tg2	$⊢ (o \in topGen (c) \land t \in o) \to \exists d \in c (t \in d \land d \subseteq o)$
75	72 73 74	syl2anc	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to \exists d \in c (t \in d \land d \subseteq o)$
76		bastg	$⊢ c \in TopBases \to c \subseteq topGen (c)$
77	76	ad2antrl	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to c \subseteq topGen (c)$
78	77	ad2antrr	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to c \subseteq topGen (c)$
79	1	eqeq2i	$⊢ topGen (c) = J \leftrightarrow topGen (c) = topGen (B)$
80	79	biimpi	$⊢ topGen (c) = J \to topGen (c) = topGen (B)$
81	80	adantl	$⊢ (c ≼ ω \land topGen (c) = J) \to topGen (c) = topGen (B)$
82	81	ad2antll	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to topGen (c) = topGen (B)$
83	82	ad2antrr	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to topGen (c) = topGen (B)$
84	78 83	sseqtrd	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to c \subseteq topGen (B)$
85		simprl	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to d \in c$
86	84 85	sseldd	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to d \in topGen (B)$
87		simprrl	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to t \in d$
88		tg2	$⊢ (d \in topGen (B) \land t \in d) \to \exists m \in B (t \in m \land m \subseteq d)$
89	86 87 88	syl2anc	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to \exists m \in B (t \in m \land m \subseteq d)$
90	65	ad3antrrr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to B \subseteq topGen (B)$
91	90	ad2antrr	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to B \subseteq topGen (B)$
92	71	ad2antrr	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to topGen (c) = J$
93	92 1	eqtr2di	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to topGen (B) = topGen (c)$
94	91 93	sseqtrd	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to B \subseteq topGen (c)$
95		simprl	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to m \in B$
96	94 95	sseldd	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to m \in topGen (c)$
97		simprrl	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to t \in m$
98		tg2	$⊢ (m \in topGen (c) \land t \in m) \to \exists n \in c (t \in n \land n \subseteq m)$
99	96 97 98	syl2anc	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to \exists n \in c (t \in n \land n \subseteq m)$
100		ffn	$⊢ f : S ⟶ B \to f Fn S$
101	100	ad2antrr	$⊢ ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o)) \to f Fn S$
102	101	ad2antlr	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to f Fn S$
103	102	ad2antrr	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to f Fn S$
104		simprl	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to n \in c$
105	85	ad2antrr	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to d \in c$
106		simplrl	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to m \in B$
107		simprrr	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to n \subseteq m$
108		simprr	$⊢ (m \in B \land (t \in m \land m \subseteq d)) \to m \subseteq d$
109	108	ad2antlr	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to m \subseteq d$
110		sseq2	$⊢ w = m \to (n \subseteq w \leftrightarrow n \subseteq m)$
111		sseq1	$⊢ w = m \to (w \subseteq d \leftrightarrow m \subseteq d)$
112	110 111	anbi12d	$⊢ w = m \to ((n \subseteq w \land w \subseteq d) \leftrightarrow (n \subseteq m \land m \subseteq d))$
113	112	rspcev	$⊢ (m \in B \land (n \subseteq m \land m \subseteq d)) \to \exists w \in B (n \subseteq w \land w \subseteq d)$
114	106 107 109 113	syl12anc	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to \exists w \in B (n \subseteq w \land w \subseteq d)$
115		df-br	$⊢ n S d \leftrightarrow ⟨n, d⟩ \in S$
116		vex	$⊢ n \in V$
117		vex	$⊢ d \in V$
118		simpl	$⊢ (u = n \land v = d) \to u = n$
119	118	eleq1d	$⊢ (u = n \land v = d) \to (u \in c \leftrightarrow n \in c)$
120		simpr	$⊢ (u = n \land v = d) \to v = d$
121	120	eleq1d	$⊢ (u = n \land v = d) \to (v \in c \leftrightarrow d \in c)$
122		sseq1	$⊢ u = n \to (u \subseteq w \leftrightarrow n \subseteq w)$
123		sseq2	$⊢ v = d \to (w \subseteq v \leftrightarrow w \subseteq d)$
124	122 123	bi2anan9	$⊢ (u = n \land v = d) \to ((u \subseteq w \land w \subseteq v) \leftrightarrow (n \subseteq w \land w \subseteq d))$
125	124	rexbidv	$⊢ (u = n \land v = d) \to (\exists w \in B (u \subseteq w \land w \subseteq v) \leftrightarrow \exists w \in B (n \subseteq w \land w \subseteq d))$
126	119 121 125	3anbi123d	$⊢ (u = n \land v = d) \to ((u \in c \land v \in c \land \exists w \in B (u \subseteq w \land w \subseteq v)) \leftrightarrow (n \in c \land d \in c \land \exists w \in B (n \subseteq w \land w \subseteq d)))$
127	116 117 126 2	braba	$⊢ n S d \leftrightarrow (n \in c \land d \in c \land \exists w \in B (n \subseteq w \land w \subseteq d))$
128	115 127	bitr3i	$⊢ ⟨n, d⟩ \in S \leftrightarrow (n \in c \land d \in c \land \exists w \in B (n \subseteq w \land w \subseteq d))$
129	104 105 114 128	syl3anbrc	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to ⟨n, d⟩ \in S$
130		fnfvelrn	$⊢ (f Fn S \land ⟨n, d⟩ \in S) \to f (⟨n, d⟩) \in ran f$
131	103 129 130	syl2anc	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to f (⟨n, d⟩) \in ran f$
132		simprl	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to n \in c$
133		simplll	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to d \in c$
134		simplrl	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to m \in B$
135		simprrr	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to n \subseteq m$
136	108	ad2antlr	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to m \subseteq d$
137	134 135 136 113	syl12anc	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to \exists w \in B (n \subseteq w \land w \subseteq d)$
138	132 133 137 128	syl3anbrc	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to ⟨n, d⟩ \in S$
139		fveq2	$⊢ x = ⟨n, d⟩ \to 1^{st} (x) = 1^{st} (⟨n, d⟩)$
140		fveq2	$⊢ x = ⟨n, d⟩ \to f (x) = f (⟨n, d⟩)$
141	139 140	sseq12d	$⊢ x = ⟨n, d⟩ \to (1^{st} (x) \subseteq f (x) \leftrightarrow 1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩))$
142		fveq2	$⊢ x = ⟨n, d⟩ \to 2^{nd} (x) = 2^{nd} (⟨n, d⟩)$
143	140 142	sseq12d	$⊢ x = ⟨n, d⟩ \to (f (x) \subseteq 2^{nd} (x) \leftrightarrow f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩))$
144	141 143	anbi12d	$⊢ x = ⟨n, d⟩ \to ((1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)) \leftrightarrow (1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩)))$
145	144	rspcv	$⊢ ⟨n, d⟩ \in S \to (\forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)) \to (1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩)))$
146	138 145	syl	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to (\forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)) \to (1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩)))$
147	116 117	op1st	$⊢ 1^{st} (⟨n, d⟩) = n$
148	147	sseq1i	$⊢ 1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩) \leftrightarrow n \subseteq f (⟨n, d⟩)$
149	116 117	op2nd	$⊢ 2^{nd} (⟨n, d⟩) = d$
150	149	sseq2i	$⊢ f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩) \leftrightarrow f (⟨n, d⟩) \subseteq d$
151	148 150	anbi12i	$⊢ (1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩)) \leftrightarrow (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)$
152		simprl	$⊢ ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \land (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)) \to n \subseteq f (⟨n, d⟩)$
153		simprl	$⊢ (n \in c \land (t \in n \land n \subseteq m)) \to t \in n$
154	153	ad2antlr	$⊢ ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \land (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)) \to t \in n$
155	152 154	sseldd	$⊢ ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \land (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)) \to t \in f (⟨n, d⟩)$
156		simprr	$⊢ ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \land (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)) \to f (⟨n, d⟩) \subseteq d$
157		simplrr	$⊢ ((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \to d \subseteq o$
158	157	ad2antrr	$⊢ ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \land (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)) \to d \subseteq o$
159	156 158	sstrd	$⊢ ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \land (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)) \to f (⟨n, d⟩) \subseteq o$
160	155 159	jca	$⊢ ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \land (n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d)) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o)$
161	160	ex	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to ((n \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq d) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o))$
162	151 161	biimtrid	$⊢ (((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to ((1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩)) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o))$
163	146 162	syldc	$⊢ \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)) \to ((((d \in c \land (t \in d \land d \subseteq o)) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o))$
164	163	exp4c	$⊢ \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)) \to ((d \in c \land (t \in d \land d \subseteq o)) \to ((m \in B \land (t \in m \land m \subseteq d)) \to ((n \in c \land (t \in n \land n \subseteq m)) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o))))$
165	164	ad2antlr	$⊢ ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o)) \to ((d \in c \land (t \in d \land d \subseteq o)) \to ((m \in B \land (t \in m \land m \subseteq d)) \to ((n \in c \land (t \in n \land n \subseteq m)) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o))))$
166	165	adantl	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to ((d \in c \land (t \in d \land d \subseteq o)) \to ((m \in B \land (t \in m \land m \subseteq d)) \to ((n \in c \land (t \in n \land n \subseteq m)) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o))))$
167	166	imp41	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o)$
168		eleq2	$⊢ b = f (⟨n, d⟩) \to (t \in b \leftrightarrow t \in f (⟨n, d⟩))$
169		sseq1	$⊢ b = f (⟨n, d⟩) \to (b \subseteq o \leftrightarrow f (⟨n, d⟩) \subseteq o)$
170	168 169	anbi12d	$⊢ b = f (⟨n, d⟩) \to ((t \in b \land b \subseteq o) \leftrightarrow (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o))$
171	170	rspcev	$⊢ (f (⟨n, d⟩) \in ran f \land (t \in f (⟨n, d⟩) \land f (⟨n, d⟩) \subseteq o)) \to \exists b \in ran f (t \in b \land b \subseteq o)$
172	131 167 171	syl2anc	$⊢ ((((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \land (n \in c \land (t \in n \land n \subseteq m))) \to \exists b \in ran f (t \in b \land b \subseteq o)$
173	99 172	rexlimddv	$⊢ (((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \land (m \in B \land (t \in m \land m \subseteq d))) \to \exists b \in ran f (t \in b \land b \subseteq o)$
174	89 173	rexlimddv	$⊢ ((((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \land (d \in c \land (t \in d \land d \subseteq o))) \to \exists b \in ran f (t \in b \land b \subseteq o)$
175	75 174	rexlimddv	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \land (o \in J \land t \in o))) \to \exists b \in ran f (t \in b \land b \subseteq o)$
176	175	expr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to ((o \in J \land t \in o) \to \exists b \in ran f (t \in b \land b \subseteq o))$
177	176	ralrimivv	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to \forall o \in J \forall t \in o \exists b \in ran f (t \in b \land b \subseteq o)$
178		basgen2	$⊢ (J \in Top \land ran f \subseteq J \land \forall o \in J \forall t \in o \exists b \in ran f (t \in b \land b \subseteq o)) \to topGen (ran f) = J$
179	62 68 177 178	syl3anc	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to topGen (ran f) = J$
180	179 62	eqeltrd	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to topGen (ran f) \in Top$
181		tgclb	$⊢ ran f \in TopBases \leftrightarrow topGen (ran f) \in Top$
182	180 181	sylibr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to ran f \in TopBases$
183		omelon	$⊢ ω \in On$
184	25	adantr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to S ≼ ω$
185		ondomen	$⊢ (ω \in On \land S ≼ ω) \to S \in dom card$
186	183 184 185	sylancr	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to S \in dom card$
187	100	ad2antrl	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to f Fn S$
188		dffn4	$⊢ f Fn S \leftrightarrow f : S \underset{onto}{⟶} ran f$
189	187 188	sylib	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to f : S \underset{onto}{⟶} ran f$
190		fodomnum	$⊢ S \in dom card \to (f : S \underset{onto}{⟶} ran f \to ran f ≼ S)$
191	186 189 190	sylc	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to ran f ≼ S$
192		domtr	$⊢ (ran f ≼ S \land S ≼ ω) \to ran f ≼ ω$
193	191 184 192	syl2anc	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to ran f ≼ ω$
194	179	eqcomd	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to J = topGen (ran f)$
195		breq1	$⊢ b = ran f \to (b ≼ ω \leftrightarrow ran f ≼ ω)$
196		sseq1	$⊢ b = ran f \to (b \subseteq B \leftrightarrow ran f \subseteq B)$
197		fveq2	$⊢ b = ran f \to topGen (b) = topGen (ran f)$
198	197	eqeq2d	$⊢ b = ran f \to (J = topGen (b) \leftrightarrow J = topGen (ran f))$
199	195 196 198	3anbi123d	$⊢ b = ran f \to ((b ≼ ω \land b \subseteq B \land J = topGen (b)) \leftrightarrow (ran f ≼ ω \land ran f \subseteq B \land J = topGen (ran f)))$
200	199	rspcev	$⊢ (ran f \in TopBases \land (ran f ≼ ω \land ran f \subseteq B \land J = topGen (ran f))) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b))$
201	182 193 64 194 200	syl13anc	$⊢ (((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \land (f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x)))) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b))$
202	201	ex	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to ((f : S ⟶ B \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b)))$
203	59 202	sylbid	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to ((f : S ⟶ I (B) \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b)))$
204	203	exlimdv	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to (\exists f (f : S ⟶ I (B) \land \forall x \in S (1^{st} (x) \subseteq f (x) \land f (x) \subseteq 2^{nd} (x))) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b)))$
205	56 204	mpd	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b))$
206	5 205	rexlimddv	$⊢ (B \in TopBases \land J \in 2^{nd} 𝜔) \to \exists b \in TopBases (b ≼ ω \land b \subseteq B \land J = topGen (b))$

Metamath Proof Explorer

Theorem 2ndcctbss

Proof