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