2ndcomap

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

	Ref	Expression
Hypotheses	2ndcomap.2	$⊢ Y = ⋃ K$
	2ndcomap.3	$⊢ φ \to J \in 2^{nd} 𝜔$
	2ndcomap.5	$⊢ φ \to F \in (J Cn K)$
	2ndcomap.6	$⊢ φ \to ran F = Y$
	2ndcomap.7	$⊢ (φ \land x \in J) \to F [x] \in K$
Assertion	2ndcomap	$⊢ φ \to K \in 2^{nd} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		2ndcomap.2	$⊢ Y = ⋃ K$
2		2ndcomap.3	$⊢ φ \to J \in 2^{nd} 𝜔$
3		2ndcomap.5	$⊢ φ \to F \in (J Cn K)$
4		2ndcomap.6	$⊢ φ \to ran F = Y$
5		2ndcomap.7	$⊢ (φ \land x \in J) \to F [x] \in K$
6		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
7	3 6	syl	$⊢ φ \to K \in Top$
8	7	ad2antrr	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to K \in Top$
9		simplll	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land x \in b) \to φ$
10		bastg	$⊢ b \in TopBases \to b \subseteq topGen (b)$
11	10	ad2antlr	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to b \subseteq topGen (b)$
12		simprr	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to topGen (b) = J$
13	11 12	sseqtrd	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to b \subseteq J$
14	13	sselda	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land x \in b) \to x \in J$
15	9 14 5	syl2anc	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land x \in b) \to F [x] \in K$
16	15	fmpttd	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to (x \in b ⟼ F [x]) : b ⟶ K$
17	16	frnd	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to ran (x \in b ⟼ F [x]) \subseteq K$
18		elunii	$⊢ (z \in k \land k \in K) \to z \in ⋃ K$
19	18 1	eleqtrrdi	$⊢ (z \in k \land k \in K) \to z \in Y$
20	19	ancoms	$⊢ (k \in K \land z \in k) \to z \in Y$
21	20	adantl	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to z \in Y$
22	4	ad3antrrr	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to ran F = Y$
23	21 22	eleqtrrd	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to z \in ran F$
24		eqid	$⊢ ⋃ J = ⋃ J$
25	24 1	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ Y$
26	3 25	syl	$⊢ φ \to F : ⋃ J ⟶ Y$
27	26	ad3antrrr	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to F : ⋃ J ⟶ Y$
28		ffn	$⊢ F : ⋃ J ⟶ Y \to F Fn ⋃ J$
29		fvelrnb	$⊢ F Fn ⋃ J \to (z \in ran F \leftrightarrow \exists t \in ⋃ J F (t) = z)$
30	27 28 29	3syl	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to (z \in ran F \leftrightarrow \exists t \in ⋃ J F (t) = z)$
31	23 30	mpbid	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to \exists t \in ⋃ J F (t) = z$
32	3	ad3antrrr	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to F \in (J Cn K)$
33		simprll	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to k \in K$
34		cnima	$⊢ (F \in (J Cn K) \land k \in K) \to F^{-1} [k] \in J$
35	32 33 34	syl2anc	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to F^{-1} [k] \in J$
36	12	adantr	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to topGen (b) = J$
37	35 36	eleqtrrd	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to F^{-1} [k] \in topGen (b)$
38		simprrl	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to t \in ⋃ J$
39		simprrr	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to F (t) = z$
40		simprlr	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to z \in k$
41	39 40	eqeltrd	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to F (t) \in k$
42	27	ffnd	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to F Fn ⋃ J$
43	42	adantrr	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to F Fn ⋃ J$
44		elpreima	$⊢ F Fn ⋃ J \to (t \in F^{-1} [k] \leftrightarrow (t \in ⋃ J \land F (t) \in k))$
45	43 44	syl	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to (t \in F^{-1} [k] \leftrightarrow (t \in ⋃ J \land F (t) \in k))$
46	38 41 45	mpbir2and	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to t \in F^{-1} [k]$
47		tg2	$⊢ (F^{-1} [k] \in topGen (b) \land t \in F^{-1} [k]) \to \exists m \in b (t \in m \land m \subseteq F^{-1} [k])$
48	37 46 47	syl2anc	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to \exists m \in b (t \in m \land m \subseteq F^{-1} [k])$
49		simprl	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to m \in b$
50		eqid	$⊢ F [m] = F [m]$
51		imaeq2	$⊢ x = m \to F [x] = F [m]$
52	51	rspceeqv	$⊢ (m \in b \land F [m] = F [m]) \to \exists x \in b F [m] = F [x]$
53	49 50 52	sylancl	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to \exists x \in b F [m] = F [x]$
54	43	adantr	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to F Fn ⋃ J$
55		fnfun	$⊢ F Fn ⋃ J \to Fun F$
56	54 55	syl	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to Fun F$
57		simprrr	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to m \subseteq F^{-1} [k]$
58		funimass2	$⊢ (Fun F \land m \subseteq F^{-1} [k]) \to F [m] \subseteq k$
59	56 57 58	syl2anc	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to F [m] \subseteq k$
60		vex	$⊢ k \in V$
61		ssexg	$⊢ (F [m] \subseteq k \land k \in V) \to F [m] \in V$
62	59 60 61	sylancl	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to F [m] \in V$
63		eqid	$⊢ (x \in b ⟼ F [x]) = (x \in b ⟼ F [x])$
64	63	elrnmpt	$⊢ F [m] \in V \to (F [m] \in ran (x \in b ⟼ F [x]) \leftrightarrow \exists x \in b F [m] = F [x])$
65	62 64	syl	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to (F [m] \in ran (x \in b ⟼ F [x]) \leftrightarrow \exists x \in b F [m] = F [x])$
66	53 65	mpbird	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to F [m] \in ran (x \in b ⟼ F [x])$
67	39	adantr	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to F (t) = z$
68		simprrl	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to t \in m$
69		cnvimass	$⊢ F^{-1} [k] \subseteq dom F$
70	57 69	sstrdi	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to m \subseteq dom F$
71		funfvima2	$⊢ (Fun F \land m \subseteq dom F) \to (t \in m \to F (t) \in F [m])$
72	56 70 71	syl2anc	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to (t \in m \to F (t) \in F [m])$
73	68 72	mpd	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to F (t) \in F [m]$
74	67 73	eqeltrrd	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to z \in F [m]$
75		eleq2	$⊢ w = F [m] \to (z \in w \leftrightarrow z \in F [m])$
76		sseq1	$⊢ w = F [m] \to (w \subseteq k \leftrightarrow F [m] \subseteq k)$
77	75 76	anbi12d	$⊢ w = F [m] \to ((z \in w \land w \subseteq k) \leftrightarrow (z \in F [m] \land F [m] \subseteq k))$
78	77	rspcev	$⊢ (F [m] \in ran (x \in b ⟼ F [x]) \land (z \in F [m] \land F [m] \subseteq k)) \to \exists w \in ran (x \in b ⟼ F [x]) (z \in w \land w \subseteq k)$
79	66 74 59 78	syl12anc	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \land (m \in b \land (t \in m \land m \subseteq F^{-1} [k]))) \to \exists w \in ran (x \in b ⟼ F [x]) (z \in w \land w \subseteq k)$
80	48 79	rexlimddv	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land ((k \in K \land z \in k) \land (t \in ⋃ J \land F (t) = z))) \to \exists w \in ran (x \in b ⟼ F [x]) (z \in w \land w \subseteq k)$
81	80	anassrs	$⊢ ((((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \land (t \in ⋃ J \land F (t) = z)) \to \exists w \in ran (x \in b ⟼ F [x]) (z \in w \land w \subseteq k)$
82	31 81	rexlimddv	$⊢ (((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \land (k \in K \land z \in k)) \to \exists w \in ran (x \in b ⟼ F [x]) (z \in w \land w \subseteq k)$
83	82	ralrimivva	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to \forall k \in K \forall z \in k \exists w \in ran (x \in b ⟼ F [x]) (z \in w \land w \subseteq k)$
84		basgen2	$⊢ (K \in Top \land ran (x \in b ⟼ F [x]) \subseteq K \land \forall k \in K \forall z \in k \exists w \in ran (x \in b ⟼ F [x]) (z \in w \land w \subseteq k)) \to topGen (ran (x \in b ⟼ F [x])) = K$
85	8 17 83 84	syl3anc	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to topGen (ran (x \in b ⟼ F [x])) = K$
86	85 8	eqeltrd	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to topGen (ran (x \in b ⟼ F [x])) \in Top$
87		tgclb	$⊢ ran (x \in b ⟼ F [x]) \in TopBases \leftrightarrow topGen (ran (x \in b ⟼ F [x])) \in Top$
88	86 87	sylibr	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to ran (x \in b ⟼ F [x]) \in TopBases$
89		omelon	$⊢ ω \in On$
90		simprl	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to b ≼ ω$
91		ondomen	$⊢ (ω \in On \land b ≼ ω) \to b \in dom card$
92	89 90 91	sylancr	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to b \in dom card$
93	16	ffnd	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to (x \in b ⟼ F [x]) Fn b$
94		dffn4	$⊢ (x \in b ⟼ F [x]) Fn b \leftrightarrow (x \in b ⟼ F [x]) : b \underset{onto}{⟶} ran (x \in b ⟼ F [x])$
95	93 94	sylib	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to (x \in b ⟼ F [x]) : b \underset{onto}{⟶} ran (x \in b ⟼ F [x])$
96		fodomnum	$⊢ b \in dom card \to ((x \in b ⟼ F [x]) : b \underset{onto}{⟶} ran (x \in b ⟼ F [x]) \to ran (x \in b ⟼ F [x]) ≼ b)$
97	92 95 96	sylc	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to ran (x \in b ⟼ F [x]) ≼ b$
98		domtr	$⊢ (ran (x \in b ⟼ F [x]) ≼ b \land b ≼ ω) \to ran (x \in b ⟼ F [x]) ≼ ω$
99	97 90 98	syl2anc	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to ran (x \in b ⟼ F [x]) ≼ ω$
100		2ndci	$⊢ (ran (x \in b ⟼ F [x]) \in TopBases \land ran (x \in b ⟼ F [x]) ≼ ω) \to topGen (ran (x \in b ⟼ F [x])) \in 2^{nd} 𝜔$
101	88 99 100	syl2anc	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to topGen (ran (x \in b ⟼ F [x])) \in 2^{nd} 𝜔$
102	85 101	eqeltrrd	$⊢ ((φ \land b \in TopBases) \land (b ≼ ω \land topGen (b) = J)) \to K \in 2^{nd} 𝜔$
103		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists b \in TopBases (b ≼ ω \land topGen (b) = J)$
104	2 103	sylib	$⊢ φ \to \exists b \in TopBases (b ≼ ω \land topGen (b) = J)$
105	102 104	r19.29a	$⊢ φ \to K \in 2^{nd} 𝜔$

Metamath Proof Explorer

Theorem 2ndcomap

Proof