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	⊢ 𝐽 = ( topGen ‘ 𝐵 )
	2ndcctbss.2	⊢ 𝑆 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) }
Assertion	2ndcctbss	⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) )

Proof

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

Metamath Proof Explorer

Theorem 2ndcctbss

Proof