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 23414

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 23197	. . . . . 6 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Top)
4	3	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ Top)
5		simplll 775	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → 𝜑)
6		bastg 22922	. . . . . . . . . 10 ⊢ (𝑏 ∈ TopBases → 𝑏 ⊆ (topGen‘𝑏))
7	6	ad2antlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ (topGen‘𝑏))
8		simprr 773	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘𝑏) = 𝐽)
9	7, 8	sseqtrd 3972	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ 𝐽)
10	9	sselda 3935	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ 𝐽)
11		2ndcomap.7	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾)
12	5, 10, 11	syl2anc 585	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → (𝐹 “ 𝑥) ∈ 𝐾)
13	12	fmpttd 7069	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏⟶𝐾)
14	13	frnd 6678	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ⊆ 𝐾)
15		elunii 4870	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾) → 𝑧 ∈ ∪ 𝐾)
16		2ndcomap.2	. . . . . . . . . . 11 ⊢ 𝑌 = ∪ 𝐾
17	15, 16	eleqtrrdi 2848	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾) → 𝑧 ∈ 𝑌)
18	17	ancoms 458	. . . . . . . . 9 ⊢ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) → 𝑧 ∈ 𝑌)
19	18	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝑧 ∈ 𝑌)
20		2ndcomap.6	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = 𝑌)
21	20	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ran 𝐹 = 𝑌)
22	19, 21	eleqtrrd 2840	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝑧 ∈ ran 𝐹)
23		eqid 2737	. . . . . . . . . . 11 ⊢ ∪ 𝐽 = ∪ 𝐽
24	23, 16	cnf 23202	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝑌)
25	1, 24	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:∪ 𝐽⟶𝑌)
26	25	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝐹:∪ 𝐽⟶𝑌)
27		ffn 6670	. . . . . . . 8 ⊢ (𝐹:∪ 𝐽⟶𝑌 → 𝐹 Fn ∪ 𝐽)
28		fvelrnb 6902	. . . . . . . 8 ⊢ (𝐹 Fn ∪ 𝐽 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧))
29	26, 27, 28	3syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧))
30	22, 29	mpbid 232	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧)
31	1	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝐹 ∈ (𝐽 Cn 𝐾))
32		simprll 779	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑘 ∈ 𝐾)
33		cnima 23221	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑘 ∈ 𝐾) → (^◡𝐹 “ 𝑘) ∈ 𝐽)
34	31, 32, 33	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (^◡𝐹 “ 𝑘) ∈ 𝐽)
35	8	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (topGen‘𝑏) = 𝐽)
36	34, 35	eleqtrrd 2840	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (^◡𝐹 “ 𝑘) ∈ (topGen‘𝑏))
37		simprrl 781	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑡 ∈ ∪ 𝐽)
38		simprrr 782	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝐹‘𝑡) = 𝑧)
39		simprlr 780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑧 ∈ 𝑘)
40	38, 39	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝐹‘𝑡) ∈ 𝑘)
41	26	ffnd 6671	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝐹 Fn ∪ 𝐽)
42	41	adantrr 718	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝐹 Fn ∪ 𝐽)
43		elpreima 7012	. . . . . . . . . . 11 ⊢ (𝐹 Fn ∪ 𝐽 → (𝑡 ∈ (^◡𝐹 “ 𝑘) ↔ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) ∈ 𝑘)))
44	42, 43	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝑡 ∈ (^◡𝐹 “ 𝑘) ↔ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) ∈ 𝑘)))
45	37, 40, 44	mpbir2and 714	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑡 ∈ (^◡𝐹 “ 𝑘))
46		tg2 22921	. . . . . . . . 9 ⊢ (((^◡𝐹 “ 𝑘) ∈ (topGen‘𝑏) ∧ 𝑡 ∈ (^◡𝐹 “ 𝑘)) → ∃𝑚 ∈ 𝑏 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))
47	36, 45, 46	syl2anc 585	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → ∃𝑚 ∈ 𝑏 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))
48		simprl 771	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑚 ∈ 𝑏)
49		eqid 2737	. . . . . . . . . . 11 ⊢ (𝐹 “ 𝑚) = (𝐹 “ 𝑚)
50		imaeq2 6023	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑚 → (𝐹 “ 𝑥) = (𝐹 “ 𝑚))
51	50	rspceeqv 3601	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ 𝑏 ∧ (𝐹 “ 𝑚) = (𝐹 “ 𝑚)) → ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥))
52	48, 49, 51	sylancl 587	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥))
53	42	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝐹 Fn ∪ 𝐽)
54		fnfun 6600	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn ∪ 𝐽 → Fun 𝐹)
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → Fun 𝐹)
56		simprrr 782	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑚 ⊆ (^◡𝐹 “ 𝑘))
57		funimass2 6583	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)) → (𝐹 “ 𝑚) ⊆ 𝑘)
58	55, 56, 57	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ⊆ 𝑘)
59		vex 3446	. . . . . . . . . . . 12 ⊢ 𝑘 ∈ V
60		ssexg 5270	. . . . . . . . . . . 12 ⊢ (((𝐹 “ 𝑚) ⊆ 𝑘 ∧ 𝑘 ∈ V) → (𝐹 “ 𝑚) ∈ V)
61	58, 59, 60	sylancl 587	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ∈ V)
62		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) = (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))
63	62	elrnmpt 5915	. . . . . . . . . . 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 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑡 ∈ 𝑚)
68		cnvimass 6049	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 “ 𝑘) ⊆ dom 𝐹
69	56, 68	sstrdi 3948	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑚 ⊆ dom 𝐹)
70		funfvima2 7187	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑚 ⊆ dom 𝐹) → (𝑡 ∈ 𝑚 → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚)))
71	55, 69, 70	syl2anc 585	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝑡 ∈ 𝑚 → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚)))
72	67, 71	mpd 15	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚))
73	66, 72	eqeltrrd 2838	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → 𝑧 ∈ (𝐹 “ 𝑚))
74		eleq2 2826	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹 “ 𝑚) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ (𝐹 “ 𝑚)))
75		sseq1 3961	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹 “ 𝑚) → (𝑤 ⊆ 𝑘 ↔ (𝐹 “ 𝑚) ⊆ 𝑘))
76	74, 75	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑤 = (𝐹 “ 𝑚) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘) ↔ (𝑧 ∈ (𝐹 “ 𝑚) ∧ (𝐹 “ 𝑚) ⊆ 𝑘)))
77	76	rspcev 3578	. . . . . . . . 9 ⊢ (((𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∧ (𝑧 ∈ (𝐹 “ 𝑚) ∧ (𝐹 “ 𝑚) ⊆ 𝑘)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
78	65, 73, 58, 77	syl12anc 837	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (^◡𝐹 “ 𝑘)))) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
79	47, 78	rexlimddv 3145	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
80	79	anassrs 467	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
81	30, 80	rexlimddv 3145	. . . . 5 ⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
82	81	ralrimivva 3181	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ∀𝑘 ∈ 𝐾 ∀𝑧 ∈ 𝑘 ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘))
83		basgen2 22945	. . . 4 ⊢ ((𝐾 ∈ Top ∧ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ⊆ 𝐾 ∧ ∀𝑘 ∈ 𝐾 ∀𝑧 ∈ 𝑘 ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) = 𝐾)
84	4, 14, 82, 83	syl3anc 1374	. . 3 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) = 𝐾)
85	84, 4	eqeltrd 2837	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ Top)
86		tgclb 22926	. . . . 5 ⊢ (ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ Top)
87	85, 86	sylibr 234	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases)
88		omelon 9567	. . . . . . 7 ⊢ ω ∈ On
89		simprl 771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ≼ ω)
90		ondomen 9959	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝑏 ≼ ω) → 𝑏 ∈ dom card)
91	88, 89, 90	sylancr 588	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ∈ dom card)
92	13	ffnd 6671	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) Fn 𝑏)
93		dffn4 6760	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) Fn 𝑏 ↔ (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)))
94	92, 93	sylib 218	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)))
95		fodomnum 9979	. . . . . 6 ⊢ (𝑏 ∈ dom card → ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏))
96	91, 94, 95	sylc 65	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏)
97		domtr 8956	. . . . 5 ⊢ ((ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏 ∧ 𝑏 ≼ ω) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω)
98	96, 89, 97	syl2anc 585	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω)
99		2ndci 23404	. . . 4 ⊢ ((ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases ∧ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ 2^ndω)
100	87, 98, 99	syl2anc 585	. . 3 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ 2^ndω)
101	84, 100	eqeltrrd 2838	. 2 ⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ 2^ndω)
102		2ndcomap.3	. . 3 ⊢ (𝜑 → 𝐽 ∈ 2^ndω)
103		is2ndc 23402	. . 3 ⊢ (𝐽 ∈ 2^ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
104	102, 103	sylib 218	. 2 ⊢ (𝜑 → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
105	101, 104	r19.29a 3146	1 ⊢ (𝜑 → 𝐾 ∈ 2^ndω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ⊆ wss 3903 ∪ cuni 4865 class class class wbr 5100 ↦ cmpt 5181 ^◡ccnv 5631 dom cdm 5632 ran crn 5633 “ cima 5635 Oncon0 6325 Fun wfun 6494 Fn wfn 6495 ⟶wf 6496 –onto→wfo 6498 ‘cfv 6500 (class class class)co 7368 ωcom 7818 ≼ cdom 8893 cardccrd 9859 topGenctg 17369 Topctop 22849 TopBasesctb 22901 Cn ccn 23180 2^ndωc2ndc 23394

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-er 8645 df-map 8777 df-en 8896 df-dom 8897 df-card 9863 df-acn 9866 df-topgen 17375 df-top 22850 df-topon 22867 df-bases 22902 df-cn 23183 df-2ndc 23396

This theorem is referenced by: (None)

W3C validator