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	relopabi	⊢ 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	48	rexeqdv	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1^st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2^nd ‘ 𝑥 ) ) ↔ ∃ 𝑤 ∈ 𝐵 ( ( 1^st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2^nd ‘ 𝑥 ) ) ) )
50	46 49	mpbird	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1^st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2^nd ‘ 𝑥 ) ) )
51	50	ralrimiva	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1^st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2^nd ‘ 𝑥 ) ) )
52		fvex	⊢ ( I ‘ 𝐵 ) ∈ V
53		sseq2	⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( ( 1^st ‘ 𝑥 ) ⊆ 𝑤 ↔ ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ) )
54		sseq1	⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( 𝑤 ⊆ ( 2^nd ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) )
55	53 54	anbi12d	⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( ( ( 1^st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2^nd ‘ 𝑥 ) ) ↔ ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) )
56	52 55	axcc4dom	⊢ ( ( 𝑆 ≼ ω ∧ ∀ 𝑥 ∈ 𝑆 ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1^st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2^nd ‘ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) )
57	25 51 56	syl2anc	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) )
58	47	ad2antrr	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( I ‘ 𝐵 ) = 𝐵 )
59	58	feq3d	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ↔ 𝑓 : 𝑆 ⟶ 𝐵 ) )
60	59	anbi1d	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ↔ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) )
61		2ndctop	⊢ ( 𝐽 ∈ 2^ndω → 𝐽 ∈ Top )
62	61	adantl	⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) → 𝐽 ∈ Top )
63	62	ad2antrr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝐽 ∈ Top )
64		frn	⊢ ( 𝑓 : 𝑆 ⟶ 𝐵 → ran 𝑓 ⊆ 𝐵 )
65	64	ad2antrl	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ⊆ 𝐵 )
66		bastg	⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
67	66	ad3antrrr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
68	67 1	sseqtrrdi	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝐵 ⊆ 𝐽 )
69	65 68	sstrd	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ⊆ 𝐽 )
70		simprrl	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝑜 ∈ 𝐽 )
71		simprr	⊢ ( ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) → ( topGen ‘ 𝑐 ) = 𝐽 )
72	71	ad2antlr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ( topGen ‘ 𝑐 ) = 𝐽 )
73	70 72	eleqtrrd	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝑜 ∈ ( topGen ‘ 𝑐 ) )
74		simprrr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝑡 ∈ 𝑜 )
75		tg2	⊢ ( ( 𝑜 ∈ ( topGen ‘ 𝑐 ) ∧ 𝑡 ∈ 𝑜 ) → ∃ 𝑑 ∈ 𝑐 ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) )
76	73 74 75	syl2anc	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ∃ 𝑑 ∈ 𝑐 ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) )
77		bastg	⊢ ( 𝑐 ∈ TopBases → 𝑐 ⊆ ( topGen ‘ 𝑐 ) )
78	77	ad2antrl	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → 𝑐 ⊆ ( topGen ‘ 𝑐 ) )
79	78	ad2antrr	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑐 ⊆ ( topGen ‘ 𝑐 ) )
80	1	eqeq2i	⊢ ( ( topGen ‘ 𝑐 ) = 𝐽 ↔ ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) )
81	80	biimpi	⊢ ( ( topGen ‘ 𝑐 ) = 𝐽 → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) )
82	81	adantl	⊢ ( ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) )
83	82	ad2antll	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) )
84	83	ad2antrr	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) )
85	79 84	sseqtrd	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑐 ⊆ ( topGen ‘ 𝐵 ) )
86		simprl	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑑 ∈ 𝑐 )
87	85 86	sseldd	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑑 ∈ ( topGen ‘ 𝐵 ) )
88		simprrl	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑡 ∈ 𝑑 )
89		tg2	⊢ ( ( 𝑑 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑡 ∈ 𝑑 ) → ∃ 𝑚 ∈ 𝐵 ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) )
90	87 88 89	syl2anc	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → ∃ 𝑚 ∈ 𝐵 ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) )
91	66	ad3antrrr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
92	91	ad2antrr	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
93	72	ad2antrr	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ( topGen ‘ 𝑐 ) = 𝐽 )
94	93 1	syl6req	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝑐 ) )
95	92 94	sseqtrd	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝑐 ) )
96		simprl	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑚 ∈ 𝐵 )
97	95 96	sseldd	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑚 ∈ ( topGen ‘ 𝑐 ) )
98		simprrl	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑡 ∈ 𝑚 )
99		tg2	⊢ ( ( 𝑚 ∈ ( topGen ‘ 𝑐 ) ∧ 𝑡 ∈ 𝑚 ) → ∃ 𝑛 ∈ 𝑐 ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) )
100	97 98 99	syl2anc	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ∃ 𝑛 ∈ 𝑐 ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) )
101		ffn	⊢ ( 𝑓 : 𝑆 ⟶ 𝐵 → 𝑓 Fn 𝑆 )
102	101	ad2antrr	⊢ ( ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) → 𝑓 Fn 𝑆 )
103	102	ad2antlr	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑓 Fn 𝑆 )
104	103	ad2antrr	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑓 Fn 𝑆 )
105		simprl	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ∈ 𝑐 )
106	86	ad2antrr	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑑 ∈ 𝑐 )
107		simplrl	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ∈ 𝐵 )
108		simprrr	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ⊆ 𝑚 )
109		simprr	⊢ ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → 𝑚 ⊆ 𝑑 )
110	109	ad2antlr	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ⊆ 𝑑 )
111		sseq2	⊢ ( 𝑤 = 𝑚 → ( 𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑚 ) )
112		sseq1	⊢ ( 𝑤 = 𝑚 → ( 𝑤 ⊆ 𝑑 ↔ 𝑚 ⊆ 𝑑 ) )
113	111 112	anbi12d	⊢ ( 𝑤 = 𝑚 → ( ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ↔ ( 𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) )
114	113	rspcev	⊢ ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) )
115	107 108 110 114	syl12anc	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) )
116		df-br	⊢ ( 𝑛 𝑆 𝑑 ↔ ⟨ 𝑛 , 𝑑 ⟩ ∈ 𝑆 )
117		vex	⊢ 𝑛 ∈ V
118		vex	⊢ 𝑑 ∈ V
119		simpl	⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → 𝑢 = 𝑛 )
120	119	eleq1d	⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( 𝑢 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐 ) )
121		simpr	⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → 𝑣 = 𝑑 )
122	121	eleq1d	⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( 𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐 ) )
123		sseq1	⊢ ( 𝑢 = 𝑛 → ( 𝑢 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑤 ) )
124		sseq2	⊢ ( 𝑣 = 𝑑 → ( 𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑑 ) )
125	123 124	bi2anan9	⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ↔ ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) )
126	125	rexbidv	⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ↔ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) )
127	120 122 126	3anbi123d	⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ↔ ( 𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) ) )
128	117 118 127 2	braba	⊢ ( 𝑛 𝑆 𝑑 ↔ ( 𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) )
129	116 128	bitr3i	⊢ ( ⟨ 𝑛 , 𝑑 ⟩ ∈ 𝑆 ↔ ( 𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) )
130	105 106 115 129	syl3anbrc	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ⟨ 𝑛 , 𝑑 ⟩ ∈ 𝑆 )
131		fnfvelrn	⊢ ( ( 𝑓 Fn 𝑆 ∧ ⟨ 𝑛 , 𝑑 ⟩ ∈ 𝑆 ) → ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∈ ran 𝑓 )
132	104 130 131	syl2anc	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∈ ran 𝑓 )
133		simprl	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ∈ 𝑐 )
134		simplll	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑑 ∈ 𝑐 )
135		simplrl	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ∈ 𝐵 )
136		simprrr	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ⊆ 𝑚 )
137	109	ad2antlr	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ⊆ 𝑑 )
138	135 136 137 114	syl12anc	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) )
139	133 134 138 129	syl3anbrc	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ⟨ 𝑛 , 𝑑 ⟩ ∈ 𝑆 )
140		fveq2	⊢ ( 𝑥 = ⟨ 𝑛 , 𝑑 ⟩ → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) )
141		fveq2	⊢ ( 𝑥 = ⟨ 𝑛 , 𝑑 ⟩ → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) )
142	140 141	sseq12d	⊢ ( 𝑥 = ⟨ 𝑛 , 𝑑 ⟩ → ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ↔ ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) )
143		fveq2	⊢ ( 𝑥 = ⟨ 𝑛 , 𝑑 ⟩ → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) )
144	141 143	sseq12d	⊢ ( 𝑥 = ⟨ 𝑛 , 𝑑 ⟩ → ( ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ↔ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) )
145	142 144	anbi12d	⊢ ( 𝑥 = ⟨ 𝑛 , 𝑑 ⟩ → ( ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ↔ ( ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) ) )
146	145	rspcv	⊢ ( ⟨ 𝑛 , 𝑑 ⟩ ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) → ( ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) ) )
147	139 146	syl	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) → ( ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) ) )
148	117 118	op1st	⊢ ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) = 𝑛
149	148	sseq1i	⊢ ( ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ↔ 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) )
150	117 118	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) = 𝑑
151	150	sseq2i	⊢ ( ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ↔ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 )
152	149 151	anbi12i	⊢ ( ( ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) ↔ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) )
153		simprl	⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) ) → 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) )
154		simprl	⊢ ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → 𝑡 ∈ 𝑛 )
155	154	ad2antlr	⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) ) → 𝑡 ∈ 𝑛 )
156	153 155	sseldd	⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) ) → 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) )
157		simprr	⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) ) → ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 )
158		simplrr	⊢ ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑑 ⊆ 𝑜 )
159	158	ad2antrr	⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) ) → 𝑑 ⊆ 𝑜 )
160	157 159	sstrd	⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) ) → ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 )
161	156 160	jca	⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) )
162	161	ex	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( ( 𝑛 ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑑 ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) )
163	152 162	syl5bi	⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( ( ( 1^st ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ ( 2^nd ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) )
164	147 163	syldc	⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) → ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) )
165	164	exp4c	⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) → ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) → ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) ) ) )
166	165	ad2antlr	⊢ ( ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) → ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) → ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) ) ) )
167	166	adantl	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) → ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) ) ) )
168	167	imp41	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) )
169		eleq2	⊢ ( 𝑏 = ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) → ( 𝑡 ∈ 𝑏 ↔ 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ) )
170		sseq1	⊢ ( 𝑏 = ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) → ( 𝑏 ⊆ 𝑜 ↔ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) )
171	169 170	anbi12d	⊢ ( 𝑏 = ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) → ( ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ↔ ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) )
172	171	rspcev	⊢ ( ( ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∈ ran 𝑓 ∧ ( 𝑡 ∈ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ∧ ( 𝑓 ‘ ⟨ 𝑛 , 𝑑 ⟩ ) ⊆ 𝑜 ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) )
173	132 168 172	syl2anc	⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) )
174	100 173	rexlimddv	⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) )
175	90 174	rexlimddv	⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) )
176	76 175	rexlimddv	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) )
177	176	expr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ( ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) )
178	177	ralrimivv	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ∀ 𝑜 ∈ 𝐽 ∀ 𝑡 ∈ 𝑜 ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) )
179		basgen2	⊢ ( ( 𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ∀ 𝑜 ∈ 𝐽 ∀ 𝑡 ∈ 𝑜 ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) → ( topGen ‘ ran 𝑓 ) = 𝐽 )
180	63 69 178 179	syl3anc	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ( topGen ‘ ran 𝑓 ) = 𝐽 )
181	180 63	eqeltrd	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ( topGen ‘ ran 𝑓 ) ∈ Top )
182		tgclb	⊢ ( ran 𝑓 ∈ TopBases ↔ ( topGen ‘ ran 𝑓 ) ∈ Top )
183	181 182	sylibr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ∈ TopBases )
184		omelon	⊢ ω ∈ On
185	25	adantr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝑆 ≼ ω )
186		ondomen	⊢ ( ( ω ∈ On ∧ 𝑆 ≼ ω ) → 𝑆 ∈ dom card )
187	184 185 186	sylancr	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝑆 ∈ dom card )
188	101	ad2antrl	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝑓 Fn 𝑆 )
189		dffn4	⊢ ( 𝑓 Fn 𝑆 ↔ 𝑓 : 𝑆 –onto→ ran 𝑓 )
190	188 189	sylib	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝑓 : 𝑆 –onto→ ran 𝑓 )
191		fodomnum	⊢ ( 𝑆 ∈ dom card → ( 𝑓 : 𝑆 –onto→ ran 𝑓 → ran 𝑓 ≼ 𝑆 ) )
192	187 190 191	sylc	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ≼ 𝑆 )
193		domtr	⊢ ( ( ran 𝑓 ≼ 𝑆 ∧ 𝑆 ≼ ω ) → ran 𝑓 ≼ ω )
194	192 185 193	syl2anc	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ≼ ω )
195	180	eqcomd	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → 𝐽 = ( topGen ‘ ran 𝑓 ) )
196		breq1	⊢ ( 𝑏 = ran 𝑓 → ( 𝑏 ≼ ω ↔ ran 𝑓 ≼ ω ) )
197		sseq1	⊢ ( 𝑏 = ran 𝑓 → ( 𝑏 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵 ) )
198		fveq2	⊢ ( 𝑏 = ran 𝑓 → ( topGen ‘ 𝑏 ) = ( topGen ‘ ran 𝑓 ) )
199	198	eqeq2d	⊢ ( 𝑏 = ran 𝑓 → ( 𝐽 = ( topGen ‘ 𝑏 ) ↔ 𝐽 = ( topGen ‘ ran 𝑓 ) ) )
200	196 197 199	3anbi123d	⊢ ( 𝑏 = ran 𝑓 → ( ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ↔ ( ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ ran 𝑓 ) ) ) )
201	200	rspcev	⊢ ( ( ran 𝑓 ∈ TopBases ∧ ( ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ ran 𝑓 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) )
202	183 194 65 195 201	syl13anc	⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) )
203	202	ex	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) )
204	60 203	sylbid	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) )
205	204	exlimdv	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1^st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2^nd ‘ 𝑥 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) )
206	57 205	mpd	⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) )
207	5 206	rexlimddv	⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2^ndω ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) )

Metamath Proof Explorer

Theorem 2ndcctbss

Proof