2ndcomap - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 2ndcomap		Structured version Visualization version GIF version

Theorem 2ndcomap 23366

Description: A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.)

**Hypotheses**
Ref	Expression
2ndcomap.2	⊢ 𝑌 = ∪ 𝐾
2ndcomap.3	⊢ (𝜑 → 𝐽 ∈ 2^ndω)
2ndcomap.5	⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
2ndcomap.6	⊢ (𝜑 → ran 𝐹 = 𝑌)
2ndcomap.7	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾)

**Assertion**
Ref	Expression
2ndcomap	⊢ (𝜑 → 𝐾 ∈ 2^ndω)

Distinct variable groups: 𝑥,𝐹 𝑥,𝐽 𝜑,𝑥 𝑥,𝐾 Allowed substitution hint: 𝑌(𝑥)

Proof of Theorem 2ndcomap Dummy variables 𝑘 𝑚 𝑡 𝑤 𝑧 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2ndcomap.5	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
2		cntop2 23149	. . . . . 6 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Top)
4	3	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ Top)
5		simplll 774	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → 𝜑)
6		bastg 22874	. . . . . . . . . 10 ⊢ (𝑏 ∈ TopBases → 𝑏 ⊆ (topGen‘𝑏))
7	6	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ (topGen‘𝑏))
8		simprr 772	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘𝑏) = 𝐽)
9	7, 8	sseqtrd 3969	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ 𝐽)
10	9	sselda 3932	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ 𝐽)
11		2ndcomap.7	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾)
12	5, 10, 11	syl2anc 584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → (𝐹 “ 𝑥) ∈ 𝐾)
13	12	fmpttd 7043	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏⟶𝐾)
14	13	frnd 6655	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ⊆ 𝐾)
15		elunii 4862	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾) → 𝑧 ∈ ∪ 𝐾)
16		2ndcomap.2	. . . . . . . . . . 11 ⊢ 𝑌 = ∪ 𝐾
17	15, 16	eleqtrrdi 2840	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾) → 𝑧 ∈ 𝑌)
18	17	ancoms 458	. . . . . . . . 9 ⊢ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) → 𝑧 ∈ 𝑌)
19	18	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝑧 ∈ 𝑌)
20		2ndcomap.6	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = 𝑌)
21	20	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ran 𝐹 = 𝑌)
22	19, 21	eleqtrrd 2832	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝑧 ∈ ran 𝐹)
23		eqid 2730	. . . . . . . . . . 11 ⊢ ∪ 𝐽 = ∪ 𝐽
24	23, 16	cnf 23154	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝑌)
25	1, 24	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:∪ 𝐽⟶𝑌)
26	25	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝐹:∪ 𝐽⟶𝑌)
27		ffn 6647	. . . . . . . 8 ⊢ (𝐹:∪ 𝐽⟶𝑌 → 𝐹 Fn ∪ 𝐽)
28		fvelrnb 6877	. . . . . . . 8 ⊢ (𝐹 Fn ∪ 𝐽 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧))
29	26, 27, 28	3syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧))
30	22, 29	mpbid 232	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧)
31	1	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝐹 ∈ (𝐽 Cn 𝐾))
32		simprll 778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑘 ∈ 𝐾)
33		cnima 23173	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑘 ∈ 𝐾) → (^◡𝐹 “ 𝑘) ∈ 𝐽)
34	31, 32, 33	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (^◡𝐹 “ 𝑘) ∈ 𝐽)
35	8	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (topGen‘𝑏) = 𝐽)
36	34, 35	eleqtrrd 2832	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (^◡𝐹 “ 𝑘) ∈ (topGen‘𝑏))
37		simprrl 780	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑡 ∈ ∪ 𝐽)
38		simprrr 781	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝐹‘𝑡) = 𝑧)
39		simprlr 779	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑧 ∈ 𝑘)
40	38, 39	eqeltrd 2829	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝐹‘𝑡) ∈ 𝑘)
41	26	ffnd 6648	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝐹 Fn ∪ 𝐽)
42	41	adantrr 717	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝐹 Fn ∪ 𝐽)
43		elpreima 6986	. . . . . . . . . . 11 ⊢ (𝐹 Fn ∪ 𝐽 → (𝑡 ∈ (^◡𝐹 “ 𝑘) ↔ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) ∈ 𝑘)))
44	42, 43	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝑡 ∈ (^◡𝐹 “ 𝑘) ↔ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) ∈ 𝑘)))
45	37, 40, 44	mpbir2and 713	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑡 ∈ (^◡𝐹 “ 𝑘))
46		tg2 22873	. . . . . . . . 9 ⊢ (((^◡𝐹 “ 𝑘) ∈ (topGen‘𝑏) ∧ 𝑡 ∈ (^◡𝐹 “ 𝑘)) → ∃𝑚 ∈ 𝑏 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))
47	36, 45, 46	syl2anc 584	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → ∃𝑚 ∈ 𝑏 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))
48		simprl 770	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑚 ∈ 𝑏)
49		eqid 2730	. . . . . . . . . . 11 ⊢ (𝐹 “ 𝑚) = (𝐹 “ 𝑚)
50		imaeq2 6002	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑚 → (𝐹 “ 𝑥) = (𝐹 “ 𝑚))
51	50	rspceeqv 3598	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ 𝑏 ∧ (𝐹 “ 𝑚) = (𝐹 “ 𝑚)) → ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥))
52	48, 49, 51	sylancl 586	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥))
53	42	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝐹 Fn ∪ 𝐽)
54		fnfun 6577	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn ∪ 𝐽 → Fun 𝐹)
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → Fun 𝐹)
56		simprrr 781	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑚 ⊆ (^◡𝐹 “ 𝑘))
57		funimass2 6560	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)) → (𝐹 “ 𝑚) ⊆ 𝑘)
58	55, 56, 57	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ⊆ 𝑘)
59		vex 3438	. . . . . . . . . . . 12 ⊢ 𝑘 ∈ V
60		ssexg 5259	. . . . . . . . . . . 12 ⊢ (((𝐹 “ 𝑚) ⊆ 𝑘 ∧ 𝑘 ∈ V) → (𝐹 “ 𝑚) ∈ V)
61	58, 59, 60	sylancl 586	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ∈ V)
62		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) = (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))
63	62	elrnmpt 5895	. . . . . . . . . . 11 ⊢ ((𝐹 “ 𝑚) ∈ V → ((𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥)))
64	61, 63	syl 17	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → ((𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥)))
65	52, 64	mpbird 257	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)))
66	38	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹‘𝑡) = 𝑧)
67		simprrl 780	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑡 ∈ 𝑚)
68		cnvimass 6028	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 “ 𝑘) ⊆ dom 𝐹
69	56, 68	sstrdi 3945	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑚 ⊆ dom 𝐹)
70		funfvima2 7160	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑚 ⊆ dom 𝐹) → (𝑡 ∈ 𝑚 → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚)))
71	55, 69, 70	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝑡 ∈ 𝑚 → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚)))
72	67, 71	mpd 15	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚))
73	66, 72	eqeltrrd 2830	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑧 ∈ (𝐹 “ 𝑚))
74		eleq2 2818	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹 “ 𝑚) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ (𝐹 “ 𝑚)))
75		sseq1 3958	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹 “ 𝑚) → (𝑤 ⊆ 𝑘 ↔ (𝐹 “ 𝑚) ⊆ 𝑘))
76	74, 75	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑤 = (𝐹 “ 𝑚) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘) ↔ (𝑧 ∈ (𝐹 “ 𝑚) ∧ (𝐹 “ 𝑚) ⊆ 𝑘)))
77	76	rspcev 3575	. . . . . . . . 9 ⊢ (((𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∧ (𝑧 ∈ (𝐹 “ 𝑚) ∧ (𝐹 “ 𝑚) ⊆ 𝑘)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
78	65, 73, 58, 77	syl12anc 836	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
79	47, 78	rexlimddv 3137	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
80	79	anassrs 467	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
81	30, 80	rexlimddv 3137	. . . . 5 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
82	81	ralrimivva 3173	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ∀𝑘 ∈ 𝐾 ∀𝑧 ∈ 𝑘 ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
83		basgen2 22897	. . . 4 ⊢ ((𝐾 ∈ Top ∧ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ⊆ 𝐾 ∧ ∀𝑘 ∈ 𝐾 ∀𝑧 ∈ 𝑘 ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) = 𝐾)
84	4, 14, 82, 83	syl3anc 1373	. . 3 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) = 𝐾)
85	84, 4	eqeltrd 2829	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ Top)
86		tgclb 22878	. . . . 5 ⊢ (ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ Top)
87	85, 86	sylibr 234	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases)
88		omelon 9531	. . . . . . 7 ⊢ ω ∈ On
89		simprl 770	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ≼ ω)
90		ondomen 9920	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝑏 ≼ ω) → 𝑏 ∈ dom card)
91	88, 89, 90	sylancr 587	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ∈ dom card)
92	13	ffnd 6648	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) Fn 𝑏)
93		dffn4 6737	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) Fn 𝑏 ↔ (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)))
94	92, 93	sylib 218	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)))
95		fodomnum 9940	. . . . . 6 ⊢ (𝑏 ∈ dom card → ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏))
96	91, 94, 95	sylc 65	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏)
97		domtr 8924	. . . . 5 ⊢ ((ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏 ∧ 𝑏 ≼ ω) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω)
98	96, 89, 97	syl2anc 584	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω)
99		2ndci 23356	. . . 4 ⊢ ((ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases ∧ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ 2^ndω)
100	87, 98, 99	syl2anc 584	. . 3 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ 2^ndω)
101	84, 100	eqeltrrd 2830	. 2 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ 2^ndω)
102		2ndcomap.3	. . 3 ⊢ (𝜑 → 𝐽 ∈ 2^ndω)
103		is2ndc 23354	. . 3 ⊢ (𝐽 ∈ 2^ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
104	102, 103	sylib 218	. 2 ⊢ (𝜑 → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
105	101, 104	r19.29a 3138	1 ⊢ (𝜑 → 𝐾 ∈ 2^ndω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2110 ∀wral 3045 ∃wrex 3054 Vcvv 3434 ⊆ wss 3900 ∪ cuni 4857 class class class wbr 5089 ↦ cmpt 5170 ^◡ccnv 5613 dom cdm 5614 ran crn 5615 “ cima 5617 Oncon0 6302 Fun wfun 6471 Fn wfn 6472 ⟶wf 6473 –onto→wfo 6475 ‘cfv 6477 (class class class)co 7341 ωcom 7791 ≼ cdom 8862 cardccrd 9820 topGenctg 17333 Topctop 22801 TopBasesctb 22853 Cn ccn 23132 2^ndωc2ndc 23346

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-inf2 9526

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-isom 6486 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-er 8617 df-map 8747 df-en 8865 df-dom 8866 df-card 9824 df-acn 9827 df-topgen 17339 df-top 22802 df-topon 22819 df-bases 22854 df-cn 23135 df-2ndc 23348

This theorem is referenced by: (None)

W3C validator