Theorem 2ndcctbss 23721

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		is2ndc 23711	. . 3 ⊢ (𝐽 ∈ 2ndω ↔ ∃𝑐 ∈ TopBases (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))
2	1	bilani 510	. 2 ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → ∃𝑐 ∈ TopBases (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))
3		vex 3454	. . . . . . 7 ⊢ 𝑐 ∈ V
4	3, 3	xpex 7751	. . . . . 6 ⊢ (𝑐 × 𝑐) ∈ V
5		3simpa 1166	. . . . . . . 8 ⊢ ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐))
6	5	ssopab2i 5522	. . . . . . 7 ⊢ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
7		2ndcctbss.2	. . . . . . 7 ⊢ 𝑆 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))}
8		df-xp 5654	. . . . . . 7 ⊢ (𝑐 × 𝑐) = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
9	6, 7, 8	3sstr4i 3982	. . . . . 6 ⊢ 𝑆 ⊆ (𝑐 × 𝑐)
10		ssdomg 9006	. . . . . 6 ⊢ ((𝑐 × 𝑐) ∈ V → (𝑆 ⊆ (𝑐 × 𝑐) → 𝑆 ≼ (𝑐 × 𝑐)))
11	4, 9, 10	mp2 9	. . . . 5 ⊢ 𝑆 ≼ (𝑐 × 𝑐)
12	3	xpdom1 9074	. . . . . . . . 9 ⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × 𝑐))
13		omex 9622	. . . . . . . . . 10 ⊢ ω ∈ V
14	13	xpdom2 9070	. . . . . . . . 9 ⊢ (𝑐 ≼ ω → (ω × 𝑐) ≼ (ω × ω))
15		domtr 9013	. . . . . . . . 9 ⊢ (((𝑐 × 𝑐) ≼ (ω × 𝑐) ∧ (ω × 𝑐) ≼ (ω × ω)) → (𝑐 × 𝑐) ≼ (ω × ω))
16	12, 14, 15	syl2anc 596	. . . . . . . 8 ⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × ω))
17		xpomen 10051	. . . . . . . 8 ⊢ (ω × ω) ≈ ω
18		domentr 9019	. . . . . . . 8 ⊢ (((𝑐 × 𝑐) ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → (𝑐 × 𝑐) ≼ ω)
19	16, 17, 18	sylancl 598	. . . . . . 7 ⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ ω)
20	19	adantr 486	. . . . . 6 ⊢ ((𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽) → (𝑐 × 𝑐) ≼ ω)
21	20	ad2antll 742	. . . . 5 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (𝑐 × 𝑐) ≼ ω)
22		domtr 9013	. . . . 5 ⊢ ((𝑆 ≼ (𝑐 × 𝑐) ∧ (𝑐 × 𝑐) ≼ ω) → 𝑆 ≼ ω)
23	11, 21, 22	sylancr 599	. . . 4 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → 𝑆 ≼ ω)
24	7	relopabiv 5795	. . . . . . . . 9 ⊢ Rel 𝑆
25		simpr 490	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
26		1st2nd 8034	. . . . . . . . 9 ⊢ ((Rel 𝑆 ∧ 𝑥 ∈ 𝑆) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
27	24, 25, 26	sylancr 599	. . . . . . . 8 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
28	27, 25	eqeltrrd 2861	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆)
29		df-br 5104	. . . . . . . . 9 ⊢ ((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆)
30		fvex 6887	. . . . . . . . . 10 ⊢ (1st ‘𝑥) ∈ V
31		fvex 6887	. . . . . . . . . 10 ⊢ (2nd ‘𝑥) ∈ V
32		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑢 = (1st ‘𝑥))
33	32	eleq1d 2845	. . . . . . . . . . 11 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑢 ∈ 𝑐 ↔ (1st ‘𝑥) ∈ 𝑐))
34		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑣 = (2nd ‘𝑥))
35	34	eleq1d 2845	. . . . . . . . . . 11 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑣 ∈ 𝑐 ↔ (2nd ‘𝑥) ∈ 𝑐))
36		sseq1 3956	. . . . . . . . . . . . 13 ⊢ (𝑢 = (1st ‘𝑥) → (𝑢 ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ 𝑤))
37		sseq2 3957	. . . . . . . . . . . . 13 ⊢ (𝑣 = (2nd ‘𝑥) → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ (2nd ‘𝑥)))
38	36, 37	bi2anan9 650	. . . . . . . . . . . 12 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
39	38	rexbidv 3186	. . . . . . . . . . 11 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
40	33, 35, 39	3anbi123d 1464	. . . . . . . . . 10 ⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))))
41	30, 31, 40, 7	braba 5508	. . . . . . . . 9 ⊢ ((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
42	29, 41	bitr3i 280	. . . . . . . 8 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆 ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))
43	42	simp3bi 1165	. . . . . . 7 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑆 → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
44	28, 43	syl 18	. . . . . 6 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
45		fvi 6950	. . . . . . 7 ⊢ (𝐵 ∈ TopBases → ( I ‘𝐵) = 𝐵)
46	45	ad3antrrr 743	. . . . . 6 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ( I ‘𝐵) = 𝐵)
47	44, 46	rexeqtrrdv 3324	. . . . 5 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
48	47	ralrimiva 3154	. . . 4 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))
49		fvex 6887	. . . . 5 ⊢ ( I ‘𝐵) ∈ V
50		sseq2 3957	. . . . . 6 ⊢ (𝑤 = (𝑓‘𝑥) → ((1st ‘𝑥) ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ (𝑓‘𝑥)))
51		sseq1 3956	. . . . . 6 ⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ⊆ (2nd ‘𝑥) ↔ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))
52	50, 51	anbi12d 644	. . . . 5 ⊢ (𝑤 = (𝑓‘𝑥) → (((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)) ↔ ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))
53	49, 52	axcc4dom 10476	. . . 4 ⊢ ((𝑆 ≼ ω ∧ ∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))
54	23, 48, 53	syl2anc 596	. . 3 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))
55	45	ad2antrr 739	. . . . . . 7 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ( I ‘𝐵) = 𝐵)
56	55	feq3d 6683	. . . . . 6 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (𝑓:𝑆⟶( I ‘𝐵) ↔ 𝑓:𝑆⟶𝐵))
57	56	anbi1d 643	. . . . 5 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ↔ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))))
58		2ndctop 23712	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ Top)
59	58	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → 𝐽 ∈ Top)
60	59	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 ∈ Top)
61		frn 6706	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶𝐵 → ran 𝑓 ⊆ 𝐵)
62	61	ad2antrl 741	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐵)
63		bastg 23231	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
64	63	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ (topGen‘𝐵))
65		2ndcctbss.1	. . . . . . . . . . . 12 ⊢ 𝐽 = (topGen‘𝐵)
66	64, 65	sseqtrrdi 3972	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ 𝐽)
67	62, 66	sstrd 3941	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐽)
68		simprrl 793	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ 𝐽)
69		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽)) → (topGen‘𝑐) = 𝐽)
70	69	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → (topGen‘𝑐) = 𝐽)
71	68, 70	eleqtrrd 2863	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ (topGen‘𝑐))
72		simprrr 794	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑡 ∈ 𝑜)
73		tg2 23230	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑜) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))
74	71, 72, 73	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))
75		bastg 23231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ TopBases → 𝑐 ⊆ (topGen‘𝑐))
76	75	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → 𝑐 ⊆ (topGen‘𝑐))
77	76	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝑐))
78	65	eqeq2i 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((topGen‘𝑐) = 𝐽 ↔ (topGen‘𝑐) = (topGen‘𝐵))
79	78	bilani 510	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽) → (topGen‘𝑐) = (topGen‘𝐵))
80	79	ad2antll 742	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (topGen‘𝑐) = (topGen‘𝐵))
81	80	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → (topGen‘𝑐) = (topGen‘𝐵))
82	77, 81	sseqtrd 3967	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝐵))
83		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ 𝑐)
84	82, 83	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ (topGen‘𝐵))
85		simprrl 793	. . . . . . . . . . . . . . 15 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑡 ∈ 𝑑)
86		tg2 23230	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑑) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))
87	84, 85, 86	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))
88	63	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝐵 ⊆ (topGen‘𝐵))
89	88	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝐵))
90	70	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝑐) = 𝐽)
91	90, 65	eqtr2di 2812	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝐵) = (topGen‘𝑐))
92	89, 91	sseqtrd 3967	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝑐))
93		simprl 783	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ 𝐵)
94	92, 93	sseldd 3932	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ (topGen‘𝑐))
95		simprrl 793	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑡 ∈ 𝑚)
96		tg2 23230	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑚) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))
97	94, 95, 96	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))
98		ffn 6698	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:𝑆⟶𝐵 → 𝑓 Fn 𝑆)
99	98	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → 𝑓 Fn 𝑆)
100	99	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑓 Fn 𝑆)
101	100	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑓 Fn 𝑆)
102		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐)
103	83	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐)
104		simplrl 789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵)
105		simprrr 794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚)
106		simprr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → 𝑚 ⊆ 𝑑)
107	106	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑)
108		sseq2 3957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑚 → (𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑚))
109		sseq1 3956	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑚 → (𝑤 ⊆ 𝑑 ↔ 𝑚 ⊆ 𝑑))
110	108, 109	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑚 → ((𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑) ↔ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑)))
111	110	rspcev 3576	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ 𝐵 ∧ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))
112	104, 105, 107, 111	syl12anc 850	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))
113		df-br 5104	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛𝑆𝑑 ↔ ⟨𝑛, 𝑑⟩ ∈ 𝑆)
114		vex 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑛 ∈ V
115		vex 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
116		simpl 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑢 = 𝑛)
117	116	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑢 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐))
118		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑣 = 𝑑)
119	118	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
120		sseq1 3956	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑛 → (𝑢 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑤))
121		sseq2 3957	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑑 → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑑))
122	120, 121	bi2anan9 650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
123	122	rexbidv 3186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
124	117, 119, 123	3anbi123d 1464	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))))
125	114, 115, 124, 7	braba 5508	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛𝑆𝑑 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
126	113, 125	bitr3i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑛, 𝑑⟩ ∈ 𝑆 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))
127	102, 103, 112, 126	syl3anbrc 1362	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ⟨𝑛, 𝑑⟩ ∈ 𝑆)
128		fnfvelrn 7069	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 Fn 𝑆 ∧ ⟨𝑛, 𝑑⟩ ∈ 𝑆) → (𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓)
129	101, 127, 128	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓)
130		simprl 783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐)
131		simplll 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐)
132		simplrl 789	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵)
133		simprrr 794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚)
134	106	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑)
135	132, 133, 134, 111	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))
136	130, 131, 135, 126	syl3anbrc 1362	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ⟨𝑛, 𝑑⟩ ∈ 𝑆)
137		fveq2 6874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (1st ‘𝑥) = (1st ‘⟨𝑛, 𝑑⟩))
138		fveq2 6874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (𝑓‘𝑥) = (𝑓‘⟨𝑛, 𝑑⟩))
139	137, 138	sseq12d 3964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ↔ (1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩)))
140		fveq2 6874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (2nd ‘𝑥) = (2nd ‘⟨𝑛, 𝑑⟩))
141	138, 140	sseq12d 3964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → ((𝑓‘𝑥) ⊆ (2nd ‘𝑥) ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)))
142	139, 141	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ⟨𝑛, 𝑑⟩ → (((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) ↔ ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
143	142	rspcv 3572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑛, 𝑑⟩ ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
144	136, 143	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
145	114, 115	op1st 7993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1st ‘⟨𝑛, 𝑑⟩) = 𝑛
146	145	sseq1i 3959	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ↔ 𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩))
147	114, 115	op2nd 7994	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ‘⟨𝑛, 𝑑⟩) = 𝑑
148	147	sseq2i 3960	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩) ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)
149	146, 148	anbi12i 640	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)) ↔ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑))
150		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩))
151		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → 𝑡 ∈ 𝑛)
152	151	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑡 ∈ 𝑛)
153	150, 152	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩))
154		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)
155		simplrr 790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑑 ⊆ 𝑜)
156	155	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑑 ⊆ 𝑜)
157	154, 156	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)
158	153, 157	jca 521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
159	158	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ((𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
160	149, 159	biimtrid 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
161	144, 160	syldc 49	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
162	161	exp4c 438	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
163	162	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
164	163	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
165	164	imp41 431	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
166		eleq2 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → (𝑡 ∈ 𝑏 ↔ 𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩)))
167		sseq1 3956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → (𝑏 ⊆ 𝑜 ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
168	166, 167	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → ((𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜) ↔ (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
169	168	rspcev 3576	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓 ∧ (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
170	129, 165, 169	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
171	97, 170	rexlimddv 3169	. . . . . . . . . . . . . 14 ⊢ ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
172	87, 171	rexlimddv 3169	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
173	74, 172	rexlimddv 3169	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
174	173	expr 462	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ((𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)))
175	174	ralrimivv 3203	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))
176		basgen2 23254	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) → (topGen‘ran 𝑓) = 𝐽)
177	60, 67, 175, 176	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran 𝑓) = 𝐽)
178	177, 60	eqeltrd 2860	. . . . . . . 8 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran 𝑓) ∈ Top)
179		tgclb 23235	. . . . . . . 8 ⊢ (ran 𝑓 ∈ TopBases ↔ (topGen‘ran 𝑓) ∈ Top)
180	178, 179	sylibr 237	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ∈ TopBases)
181		omelon 9625	. . . . . . . . . 10 ⊢ ω ∈ On
182	23	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ≼ ω)
183		ondomen 10073	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ 𝑆 ≼ ω) → 𝑆 ∈ dom card)
184	181, 182, 183	sylancr 599	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ∈ dom card)
185	98	ad2antrl 741	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓 Fn 𝑆)
186		dffn4 6791	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑆 ↔ 𝑓:𝑆–onto→ran 𝑓)
187	185, 186	sylib 221	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓:𝑆–onto→ran 𝑓)
188		fodomnum 10093	. . . . . . . . 9 ⊢ (𝑆 ∈ dom card → (𝑓:𝑆–onto→ran 𝑓 → ran 𝑓 ≼ 𝑆))
189	184, 187, 188	sylc 66	. . . . . . . 8 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼ 𝑆)
190		domtr 9013	. . . . . . . 8 ⊢ ((ran 𝑓 ≼ 𝑆 ∧ 𝑆 ≼ ω) → ran 𝑓 ≼ ω)
191	189, 182, 190	syl2anc 596	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼ ω)
192	177	eqcomd 2766	. . . . . . 7 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 = (topGen‘ran 𝑓))
193		breq1 5106	. . . . . . . . 9 ⊢ (𝑏 = ran 𝑓 → (𝑏 ≼ ω ↔ ran 𝑓 ≼ ω))
194		sseq1 3956	. . . . . . . . 9 ⊢ (𝑏 = ran 𝑓 → (𝑏 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵))
195		fveq2 6874	. . . . . . . . . 10 ⊢ (𝑏 = ran 𝑓 → (topGen‘𝑏) = (topGen‘ran 𝑓))
196	195	eqeq2d 2771	. . . . . . . . 9 ⊢ (𝑏 = ran 𝑓 → (𝐽 = (topGen‘𝑏) ↔ 𝐽 = (topGen‘ran 𝑓)))
197	193, 194, 196	3anbi123d 1464	. . . . . . . 8 ⊢ (𝑏 = ran 𝑓 → ((𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)) ↔ (ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓))))
198	197	rspcev 3576	. . . . . . 7 ⊢ ((ran 𝑓 ∈ TopBases ∧ (ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
199	180, 191, 62, 192, 198	syl13anc 1399	. . . . . 6 ⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
200	199	ex 418	. . . . 5 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))))
201	57, 200	sylbid 243	. . . 4 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))))
202	201	exlimdv 1966	. . 3 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))))
203	54, 202	mpd 16	. 2 ⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
204	2, 203	rexlimddv 3169	1 ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3899  ⟨cop 4590   class class class wbr 5103  {copab 5167   I cid 5542   × cxp 5646  dom cdm 5648  ran crn 5649  Rel wrel 5653  Oncon0 6352   Fn wfn 6523  ⟶wf 6524  –onto→wfo 6526  ‘cfv 6528  ωcom 7861  1^st c1st 7983  2^nd c2nd 7984   ≈ cen 8949   ≼ cdom 8950  cardccrd 9973  topGenctg 17555  Topctop 23158  TopBasesctb 23210  2^ndωc2ndc 23703

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-inf2 9620  ax-cc 10470

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-se 5602  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6294  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-isom 6537  df-riota 7366  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8455  df-er 8696  df-map 8828  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-oi 9482  df-card 9977  df-acn 9980  df-topgen 17561  df-top 23159  df-bases 23211  df-2ndc 23705

This theorem is used by: (None)