Theorem 2ndcctbss 23398

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.)

Hypotheses

Ref	Expression
2ndcctbss.1	⊢ 𝐽 = (topGen‘𝐵)
2ndcctbss.2	⊢ 𝑆 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))}

Assertion

Ref	Expression
2ndcctbss	⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))

Distinct variable groups:   𝑏,𝑐,𝑢,𝑣,𝑤,𝐵   𝐽,𝑏,𝑐

Allowed substitution hints:   𝑆(𝑤,𝑣,𝑢,𝑏,𝑐)   𝐽(𝑤,𝑣,𝑢)

Proof of Theorem 2ndcctbss

Dummy variables 𝑑 𝑓 𝑚 𝑛 𝑜 𝑡 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 484	. . 3 ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → 𝐽 ∈ 2ndω)
2		is2ndc 23389	. . 3 ⊢ (𝐽 ∈ 2ndω ↔ ∃𝑐 ∈ TopBases (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))
3	1, 2	sylib 218	. 2 ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → ∃𝑐 ∈ TopBases (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))
4		vex 3468	. . . . . . 7 ⊢ 𝑐 ∈ V
5	4, 4	xpex 7752	. . . . . 6 ⊢ (𝑐 × 𝑐) ∈ V
6		3simpa 1148	. . . . . . . 8 ⊢ ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐))
7	6	ssopab2i 5530	. . . . . . 7 ⊢ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
8		2ndcctbss.2	. . . . . . 7 ⊢ 𝑆 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))}
9		df-xp 5665	. . . . . . 7 ⊢ (𝑐 × 𝑐) = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
10	7, 8, 9	3sstr4i 4015	. . . . . 6 ⊢ 𝑆 ⊆ (𝑐 × 𝑐)
11		ssdomg 9019	. . . . . 6 ⊢ ((𝑐 × 𝑐) ∈ V → (𝑆 ⊆ (𝑐 × 𝑐) → 𝑆 ≼ (𝑐 × 𝑐)))
12	5, 10, 11	mp2 9	. . . . 5 ⊢ 𝑆 ≼ (𝑐 × 𝑐)
13	4	xpdom1 9090	. . . . . . . . 9 ⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × 𝑐))
14		omex 9662	. . . . . . . . . 10 ⊢ ω ∈ V
15	14	xpdom2 9086	. . . . . . . . 9 ⊢ (𝑐 ≼ ω → (ω × 𝑐) ≼ (ω × ω))
16		domtr 9026	. . . . . . . . 9 ⊢ (((𝑐 × 𝑐) ≼ (ω × 𝑐) ∧ (ω × 𝑐) ≼ (ω × ω)) → (𝑐 × 𝑐) ≼ (ω × ω))
17	13, 15, 16	syl2anc 584	. . . . . . . 8 ⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × ω))
18		xpomen 10034	. . . . . . . 8 ⊢ (ω × ω) ≈ ω
19		domentr 9032	. . . . . . . 8 ⊢ (((𝑐 × 𝑐) ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → (𝑐 × 𝑐) ≼ ω)
20	17, 18, 19	sylancl 586	. . . . . . 7 ⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ ω)
21	20	adantr 480	. . . . . 6 ⊢ ((𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽) → (𝑐 × 𝑐) ≼ ω)
22	21	ad2antll 729	. . . . 5 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (𝑐 × 𝑐) ≼ ω)
23		domtr 9026	. . . . 5 ⊢ ((𝑆 ≼ (𝑐 × 𝑐) ∧ (𝑐 × 𝑐) ≼ ω) → 𝑆 ≼ ω)
24	12, 22, 23	sylancr 587	. . . 4 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → 𝑆 ≼ ω)
25	8	relopabiv 5804	. . . . . . . . 9 ⊢ Rel 𝑆
26		simpr 484	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
27		1st2nd 8043	. . . . . . . . 9 ⊢ ((Rel 𝑆 ∧ 𝑥 ∈ 𝑆) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
28	25, 26, 27	sylancr 587	. . . . . . . 8 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
29	28, 26	eqeltrrd 2836	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆)
30		df-br 5125	. . . . . . . . 9 ⊢ ((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆)
31		fvex 6894	. . . . . . . . . 10 ⊢ (1st ‘𝑥) ∈ V
32		fvex 6894	. . . . . . . . . 10 ⊢ (2nd ‘𝑥) ∈ V
33		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑢 = (1st ‘𝑥))
34	33	eleq1d 2820	. . . . . . . . . . 11 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑢 ∈ 𝑐 ↔ (1st ‘𝑥) ∈ 𝑐))
35		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑣 = (2nd ‘𝑥))
36	35	eleq1d 2820	. . . . . . . . . . 11 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑣 ∈ 𝑐 ↔ (2nd ‘𝑥) ∈ 𝑐))
37		sseq1 3989	. . . . . . . . . . . . 13 ⊢ (𝑢 = (1st ‘𝑥) → (𝑢 ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ 𝑤))
38		sseq2 3990	. . . . . . . . . . . . 13 ⊢ (𝑣 = (2nd ‘𝑥) → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ (2nd ‘𝑥)))
39	37, 38	bi2anan9 638	. . . . . . . . . . . 12 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
40	39	rexbidv 3165	. . . . . . . . . . 11 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
41	34, 36, 40	3anbi123d 1438	. . . . . . . . . 10 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))))
42	31, 32, 41, 8	braba 5517	. . . . . . . . 9 ⊢ ((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
43	30, 42	bitr3i 277	. . . . . . . 8 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆 ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
44	43	simp3bi 1147	. . . . . . 7 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆 → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
45	29, 44	syl 17	. . . . . 6 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
46		fvi 6960	. . . . . . 7 ⊢ (𝐵 ∈ TopBases → ( I ‘𝐵) = 𝐵)
47	46	ad3antrrr 730	. . . . . 6 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ( I ‘𝐵) = 𝐵)
48	45, 47	rexeqtrrdv 3314	. . . . 5 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
49	48	ralrimiva 3133	. . . 4 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
50		fvex 6894	. . . . 5 ⊢ ( I ‘𝐵) ∈ V
51		sseq2 3990	. . . . . 6 ⊢ (𝑤 = (𝑓‘𝑥) → ((1st ‘𝑥) ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ (𝑓‘𝑥)))
52		sseq1 3989	. . . . . 6 ⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ⊆ (2nd ‘𝑥) ↔ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))
53	51, 52	anbi12d 632	. . . . 5 ⊢ (𝑤 = (𝑓‘𝑥) → (((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)) ↔ ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))
54	50, 53	axcc4dom 10460	. . . 4 ⊢ ((𝑆 ≼ ω ∧ ∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))
55	24, 49, 54	syl2anc 584	. . 3 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))
56	46	ad2antrr 726	. . . . . . 7 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ( I ‘𝐵) = 𝐵)
57	56	feq3d 6698	. . . . . 6 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (𝑓:𝑆⟶( I ‘𝐵) ↔ 𝑓:𝑆⟶𝐵))
58	57	anbi1d 631	. . . . 5 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ↔ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))))
59		2ndctop 23390	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ Top)
60	59	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → 𝐽 ∈ Top)
61	60	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 ∈ Top)
62		frn 6718	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶𝐵 → ran 𝑓 ⊆ 𝐵)
63	62	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐵)
64		bastg 22909	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
65	64	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ (topGen‘𝐵))
66		2ndcctbss.1	. . . . . . . . . . . 12 ⊢ 𝐽 = (topGen‘𝐵)
67	65, 66	sseqtrrdi 4005	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ 𝐽)
68	63, 67	sstrd 3974	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐽)
69		simprrl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ 𝐽)
70		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽)) → (topGen‘𝑐) = 𝐽)
71	70	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → (topGen‘𝑐) = 𝐽)
72	69, 71	eleqtrrd 2838	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ (topGen‘𝑐))
73		simprrr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑡 ∈ 𝑜)
74		tg2 22908	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑜) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))
75	72, 73, 74	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))
76		bastg 22909	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ TopBases → 𝑐 ⊆ (topGen‘𝑐))
77	76	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → 𝑐 ⊆ (topGen‘𝑐))
78	77	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝑐))
79	66	eqeq2i 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((topGen‘𝑐) = 𝐽 ↔ (topGen‘𝑐) = (topGen‘𝐵))
80	79	biimpi 216	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((topGen‘𝑐) = 𝐽 → (topGen‘𝑐) = (topGen‘𝐵))
81	80	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽) → (topGen‘𝑐) = (topGen‘𝐵))
82	81	ad2antll 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (topGen‘𝑐) = (topGen‘𝐵))
83	82	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → (topGen‘𝑐) = (topGen‘𝐵))
84	78, 83	sseqtrd 4000	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝐵))
85		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ 𝑐)
86	84, 85	sseldd 3964	. . . . . . . . . . . . . . 15 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ (topGen‘𝐵))
87		simprrl 780	. . . . . . . . . . . . . . 15 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑡 ∈ 𝑑)
88		tg2 22908	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑑) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))
89	86, 87, 88	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))
90	64	ad3antrrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝐵 ⊆ (topGen‘𝐵))
91	90	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝐵))
92	71	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝑐) = 𝐽)
93	92, 66	eqtr2di 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝐵) = (topGen‘𝑐))
94	91, 93	sseqtrd 4000	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝑐))
95		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ 𝐵)
96	94, 95	sseldd 3964	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ (topGen‘𝑐))
97		simprrl 780	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑡 ∈ 𝑚)
98		tg2 22908	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑚) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))
99	96, 97, 98	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))
100		ffn 6711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:𝑆⟶𝐵 → 𝑓 Fn 𝑆)
101	100	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → 𝑓 Fn 𝑆)
102	101	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑓 Fn 𝑆)
103	102	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑓 Fn 𝑆)
104		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐)
105	85	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐)
106		simplrl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵)
107		simprrr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚)
108		simprr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → 𝑚 ⊆ 𝑑)
109	108	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑)
110		sseq2 3990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑚 → (𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑚))
111		sseq1 3989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑚 → (𝑤 ⊆ 𝑑 ↔ 𝑚 ⊆ 𝑑))
112	110, 111	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑚 → ((𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑) ↔ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑)))
113	112	rspcev 3606	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ 𝐵 ∧ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))
114	106, 107, 109, 113	syl12anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))
115		df-br 5125	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛𝑆𝑑 ↔ ⟨𝑛, 𝑑⟩ ∈ 𝑆)
116		vex 3468	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑛 ∈ V
117		vex 3468	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
118		simpl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑢 = 𝑛)
119	118	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑢 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐))
120		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑣 = 𝑑)
121	120	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
122		sseq1 3989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑛 → (𝑢 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑤))
123		sseq2 3990	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑑 → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑑))
124	122, 123	bi2anan9 638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
125	124	rexbidv 3165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
126	119, 121, 125	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))))
127	116, 117, 126, 8	braba 5517	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛𝑆𝑑 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
128	115, 127	bitr3i 277	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑛, 𝑑⟩ ∈ 𝑆 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
129	104, 105, 114, 128	syl3anbrc 1344	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ⟨𝑛, 𝑑⟩ ∈ 𝑆)
130		fnfvelrn 7075	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 Fn 𝑆 ∧ ⟨𝑛, 𝑑⟩ ∈ 𝑆) → (𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓)
131	103, 129, 130	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓)
132		simprl 770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐)
133		simplll 774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐)
134		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵)
135		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚)
136	108	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑)
137	134, 135, 136, 113	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))
138	132, 133, 137, 128	syl3anbrc 1344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ⟨𝑛, 𝑑⟩ ∈ 𝑆)
139		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (1st ‘𝑥) = (1st ‘⟨𝑛, 𝑑⟩))
140		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (𝑓‘𝑥) = (𝑓‘⟨𝑛, 𝑑⟩))
141	139, 140	sseq12d 3997	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ↔ (1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩)))
142		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (2nd ‘𝑥) = (2nd ‘⟨𝑛, 𝑑⟩))
143	140, 142	sseq12d 3997	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → ((𝑓‘𝑥) ⊆ (2nd ‘𝑥) ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)))
144	141, 143	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) ↔ ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
145	144	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑛, 𝑑⟩ ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
146	138, 145	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
147	116, 117	op1st 8001	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1st ‘⟨𝑛, 𝑑⟩) = 𝑛
148	147	sseq1i 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ↔ 𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩))
149	116, 117	op2nd 8002	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ‘⟨𝑛, 𝑑⟩) = 𝑑
150	149	sseq2i 3993	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩) ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)
151	148, 150	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)) ↔ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑))
152		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩))
153		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → 𝑡 ∈ 𝑛)
154	153	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑡 ∈ 𝑛)
155	152, 154	sseldd 3964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩))
156		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)
157		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑑 ⊆ 𝑜)
158	157	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑑 ⊆ 𝑜)
159	156, 158	sstrd 3974	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)
160	155, 159	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
161	160	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ((𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
162	151, 161	biimtrid 242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
163	146, 162	syldc 48	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
164	163	exp4c 432	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
165	164	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
166	165	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
167	166	imp41 425	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
168		eleq2 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → (𝑡 ∈ 𝑏 ↔ 𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩)))
169		sseq1 3989	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → (𝑏 ⊆ 𝑜 ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
170	168, 169	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → ((𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜) ↔ (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
171	170	rspcev 3606	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓 ∧ (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
172	131, 167, 171	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
173	99, 172	rexlimddv 3148	. . . . . . . . . . . . . 14 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
174	89, 173	rexlimddv 3148	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
175	75, 174	rexlimddv 3148	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
176	175	expr 456	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ((𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)))
177	176	ralrimivv 3186	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
178		basgen2 22932	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) → (topGen‘ran 𝑓) = 𝐽)
179	61, 68, 177, 178	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran 𝑓) = 𝐽)
180	179, 61	eqeltrd 2835	. . . . . . . 8 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran 𝑓) ∈ Top)
181		tgclb 22913	. . . . . . . 8 ⊢ (ran 𝑓 ∈ TopBases ↔ (topGen‘ran 𝑓) ∈ Top)
182	180, 181	sylibr 234	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ∈ TopBases)
183		omelon 9665	. . . . . . . . . 10 ⊢ ω ∈ On
184	24	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ≼ ω)
185		ondomen 10056	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ 𝑆 ≼ ω) → 𝑆 ∈ dom card)
186	183, 184, 185	sylancr 587	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ∈ dom card)
187	100	ad2antrl 728	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓 Fn 𝑆)
188		dffn4 6801	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑆 ↔ 𝑓:𝑆–onto→ran 𝑓)
189	187, 188	sylib 218	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓:𝑆–onto→ran 𝑓)
190		fodomnum 10076	. . . . . . . . 9 ⊢ (𝑆 ∈ dom card → (𝑓:𝑆–onto→ran 𝑓 → ran 𝑓 ≼ 𝑆))
191	186, 189, 190	sylc 65	. . . . . . . 8 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼ 𝑆)
192		domtr 9026	. . . . . . . 8 ⊢ ((ran 𝑓 ≼ 𝑆 ∧ 𝑆 ≼ ω) → ran 𝑓 ≼ ω)
193	191, 184, 192	syl2anc 584	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼ ω)
194	179	eqcomd 2742	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 = (topGen‘ran 𝑓))
195		breq1 5127	. . . . . . . . 9 ⊢ (𝑏 = ran 𝑓 → (𝑏 ≼ ω ↔ ran 𝑓 ≼ ω))
196		sseq1 3989	. . . . . . . . 9 ⊢ (𝑏 = ran 𝑓 → (𝑏 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵))
197		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑏 = ran 𝑓 → (topGen‘𝑏) = (topGen‘ran 𝑓))
198	197	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑏 = ran 𝑓 → (𝐽 = (topGen‘𝑏) ↔ 𝐽 = (topGen‘ran 𝑓)))
199	195, 196, 198	3anbi123d 1438	. . . . . . . 8 ⊢ (𝑏 = ran 𝑓 → ((𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)) ↔ (ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓))))
200	199	rspcev 3606	. . . . . . 7 ⊢ ((ran 𝑓 ∈ TopBases ∧ (ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
201	182, 193, 63, 194, 200	syl13anc 1374	. . . . . 6 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
202	201	ex 412	. . . . 5 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))))
203	58, 202	sylbid 240	. . . 4 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))))
204	203	exlimdv 1933	. . 3 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))))
205	55, 204	mpd 15	. 2 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
206	3, 205	rexlimddv 3148	1 ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061  Vcvv 3464   ⊆ wss 3931  ⟨cop 4612   class class class wbr 5124  {copab 5186   I cid 5552   × cxp 5657  dom cdm 5659  ran crn 5660  Rel wrel 5664  Oncon0 6357   Fn wfn 6531  ⟶wf 6532  –onto→wfo 6534  ‘cfv 6536  ωcom 7866  1^st c1st 7991  2^nd c2nd 7992   ≈ cen 8961   ≼ cdom 8962  cardccrd 9954  topGenctg 17456  Topctop 22836  TopBasesctb 22888  2^ndωc2ndc 23381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-inf2 9660  ax-cc 10454

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8724  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-oi 9529  df-card 9958  df-acn 9961  df-topgen 17462  df-top 22837  df-bases 22889  df-2ndc 23383

This theorem is referenced by: (None)