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	relopabi	$⊢ 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	48	rexeqdv	$⊢ (((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)) \leftrightarrow \exists w \in B (1^{st} (x) \subseteq w \land w \subseteq 2^{nd} (x)))$
50	46 49	mpbird	$⊢ (((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))$
51	50	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))$
52		fvex	$⊢ I (B) \in V$
53		sseq2	$⊢ w = f (x) \to (1^{st} (x) \subseteq w \leftrightarrow 1^{st} (x) \subseteq f (x))$
54		sseq1	$⊢ w = f (x) \to (w \subseteq 2^{nd} (x) \leftrightarrow f (x) \subseteq 2^{nd} (x))$
55	53 54	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)))$
56	52 55	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)))$
57	25 51 56	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)))$
58	47	ad2antrr	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to I (B) = B$
59	58	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)$
60	59	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))))$
61		2ndctop	$⊢ J \in 2^{nd} 𝜔 \to J \in Top$
62	61	adantl	$⊢ (B \in TopBases \land J \in 2^{nd} 𝜔) \to J \in Top$
63	62	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$
64		frn	$⊢ f : S ⟶ B \to ran f \subseteq B$
65	64	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$
66		bastg	$⊢ B \in TopBases \to B \subseteq topGen (B)$
67	66	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)$
68	67 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$
69	65 68	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$
70		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$
71		simprr	$⊢ (c \in TopBases \land (c ≼ ω \land topGen (c) = J)) \to topGen (c) = J$
72	71	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$
73	70 72	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)$
74		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$
75		tg2	$⊢ (o \in topGen (c) \land t \in o) \to \exists d \in c (t \in d \land d \subseteq o)$
76	73 74 75	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)$
77		bastg	$⊢ c \in TopBases \to c \subseteq topGen (c)$
78	77	ad2antrl	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to c \subseteq topGen (c)$
79	78	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)$
80	1	eqeq2i	$⊢ topGen (c) = J \leftrightarrow topGen (c) = topGen (B)$
81	80	biimpi	$⊢ topGen (c) = J \to topGen (c) = topGen (B)$
82	81	adantl	$⊢ (c ≼ ω \land topGen (c) = J) \to topGen (c) = topGen (B)$
83	82	ad2antll	$⊢ ((B \in TopBases \land J \in 2^{nd} 𝜔) \land (c \in TopBases \land (c ≼ ω \land topGen (c) = J))) \to topGen (c) = topGen (B)$
84	83	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)$
85	79 84	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)$
86		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$
87	85 86	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)$
88		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$
89		tg2	$⊢ (d \in topGen (B) \land t \in d) \to \exists m \in B (t \in m \land m \subseteq d)$
90	87 88 89	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)$
91	66	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)$
92	91	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)$
93	72	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$
94	93 1	syl6req	$⊢ (((((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)$
95	92 94	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)$
96		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$
97	95 96	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)$
98		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$
99		tg2	$⊢ (m \in topGen (c) \land t \in m) \to \exists n \in c (t \in n \land n \subseteq m)$
100	97 98 99	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)$
101		ffn	$⊢ f : S ⟶ B \to f Fn S$
102	101	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$
103	102	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$
104	103	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$
105		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$
106	86	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$
107		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$
108		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$
109		simprr	$⊢ (m \in B \land (t \in m \land m \subseteq d)) \to m \subseteq d$
110	109	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$
111		sseq2	$⊢ w = m \to (n \subseteq w \leftrightarrow n \subseteq m)$
112		sseq1	$⊢ w = m \to (w \subseteq d \leftrightarrow m \subseteq d)$
113	111 112	anbi12d	$⊢ w = m \to ((n \subseteq w \land w \subseteq d) \leftrightarrow (n \subseteq m \land m \subseteq d))$
114	113	rspcev	$⊢ (m \in B \land (n \subseteq m \land m \subseteq d)) \to \exists w \in B (n \subseteq w \land w \subseteq d)$
115	107 108 110 114	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)$
116		df-br	$⊢ n S d \leftrightarrow ⟨n, d⟩ \in S$
117		vex	$⊢ n \in V$
118		vex	$⊢ d \in V$
119		simpl	$⊢ (u = n \land v = d) \to u = n$
120	119	eleq1d	$⊢ (u = n \land v = d) \to (u \in c \leftrightarrow n \in c)$
121		simpr	$⊢ (u = n \land v = d) \to v = d$
122	121	eleq1d	$⊢ (u = n \land v = d) \to (v \in c \leftrightarrow d \in c)$
123		sseq1	$⊢ u = n \to (u \subseteq w \leftrightarrow n \subseteq w)$
124		sseq2	$⊢ v = d \to (w \subseteq v \leftrightarrow w \subseteq d)$
125	123 124	bi2anan9	$⊢ (u = n \land v = d) \to ((u \subseteq w \land w \subseteq v) \leftrightarrow (n \subseteq w \land w \subseteq d))$
126	125	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))$
127	120 122 126	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)))$
128	117 118 127 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))$
129	116 128	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))$
130	105 106 115 129	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$
131		fnfvelrn	$⊢ (f Fn S \land ⟨n, d⟩ \in S) \to f (⟨n, d⟩) \in ran f$
132	104 130 131	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$
133		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$
134		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$
135		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$
136		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$
137	109	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$
138	135 136 137 114	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)$
139	133 134 138 129	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$
140		fveq2	$⊢ x = ⟨n, d⟩ \to 1^{st} (x) = 1^{st} (⟨n, d⟩)$
141		fveq2	$⊢ x = ⟨n, d⟩ \to f (x) = f (⟨n, d⟩)$
142	140 141	sseq12d	$⊢ x = ⟨n, d⟩ \to (1^{st} (x) \subseteq f (x) \leftrightarrow 1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩))$
143		fveq2	$⊢ x = ⟨n, d⟩ \to 2^{nd} (x) = 2^{nd} (⟨n, d⟩)$
144	141 143	sseq12d	$⊢ x = ⟨n, d⟩ \to (f (x) \subseteq 2^{nd} (x) \leftrightarrow f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩))$
145	142 144	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⟩)))$
146	145	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⟩)))$
147	139 146	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⟩)))$
148	117 118	op1st	$⊢ 1^{st} (⟨n, d⟩) = n$
149	148	sseq1i	$⊢ 1^{st} (⟨n, d⟩) \subseteq f (⟨n, d⟩) \leftrightarrow n \subseteq f (⟨n, d⟩)$
150	117 118	op2nd	$⊢ 2^{nd} (⟨n, d⟩) = d$
151	150	sseq2i	$⊢ f (⟨n, d⟩) \subseteq 2^{nd} (⟨n, d⟩) \leftrightarrow f (⟨n, d⟩) \subseteq d$
152	149 151	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)$
153		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⟩)$
154		simprl	$⊢ (n \in c \land (t \in n \land n \subseteq m)) \to t \in n$
155	154	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$
156	153 155	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⟩)$
157		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$
158		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$
159	158	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$
160	157 159	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$
161	156 160	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)$
162	161	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))$
163	152 162	syl5bi	$⊢ (((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))$
164	147 163	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))$
165	164	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))))$
166	165	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))))$
167	166	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))))$
168	167	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)$
169		eleq2	$⊢ b = f (⟨n, d⟩) \to (t \in b \leftrightarrow t \in f (⟨n, d⟩))$
170		sseq1	$⊢ b = f (⟨n, d⟩) \to (b \subseteq o \leftrightarrow f (⟨n, d⟩) \subseteq o)$
171	169 170	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))$
172	171	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)$
173	132 168 172	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)$
174	100 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))) \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)$
175	90 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))) \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)$
176	76 175	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)$
177	176	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))$
178	177	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)$
179		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$
180	63 69 178 179	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$
181	180 63	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$
182		tgclb	$⊢ ran f \in TopBases \leftrightarrow topGen (ran f) \in Top$
183	181 182	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$
184		omelon	$⊢ ω \in On$
185	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 ≼ ω$
186		ondomen	$⊢ (ω \in On \land S ≼ ω) \to S \in dom card$
187	184 185 186	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$
188	101	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$
189		dffn4	$⊢ f Fn S \leftrightarrow f : S \underset{onto}{⟶} ran f$
190	188 189	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$
191		fodomnum	$⊢ S \in dom card \to (f : S \underset{onto}{⟶} ran f \to ran f ≼ S)$
192	187 190 191	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$
193		domtr	$⊢ (ran f ≼ S \land S ≼ ω) \to ran f ≼ ω$
194	192 185 193	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 ≼ ω$
195	180	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)$
196		breq1	$⊢ b = ran f \to (b ≼ ω \leftrightarrow ran f ≼ ω)$
197		sseq1	$⊢ b = ran f \to (b \subseteq B \leftrightarrow ran f \subseteq B)$
198		fveq2	$⊢ b = ran f \to topGen (b) = topGen (ran f)$
199	198	eqeq2d	$⊢ b = ran f \to (J = topGen (b) \leftrightarrow J = topGen (ran f))$
200	196 197 199	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)))$
201	200	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))$
202	183 194 65 195 201	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))$
203	202	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)))$
204	60 203	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)))$
205	204	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)))$
206	57 205	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))$
207	5 206	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