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

Metamath Proof Explorer

Theorem 2ndcctbss

Proof