Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ∪ 𝐾
2ndcomap.3 ⊢ ( 𝜑 → 𝐽 ∈ 2ndω )
2ndcomap.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2ndcomap.6 ⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
2ndcomap.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
Assertion 2ndcomap ( 𝜑 → 𝐾 ∈ 2ndω )

Proof

Step Hyp Ref Expression
1 2ndcomap.2 ⊢ 𝑌 = ∪ 𝐾
2 2ndcomap.3 ⊢ ( 𝜑 → 𝐽 ∈ 2ndω )
3 2ndcomap.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 2ndcomap.6 ⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
5 2ndcomap.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
6 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
7 3 6 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
8 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → 𝐾 ∈ Top )
9 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝜑 )
10 bastg ⊢ ( 𝑏 ∈ TopBases → 𝑏 ⊆ ( topGen ‘ 𝑏 ) )
11 10 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → 𝑏 ⊆ ( topGen ‘ 𝑏 ) )
12 simprr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ( topGen ‘ 𝑏 ) = 𝐽 )
13 11 12 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → 𝑏 ⊆ 𝐽 )
14 13 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝑥 ∈ 𝐽 )
15 9 14 5 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
16 15 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) : 𝑏 ⟶ 𝐾 )
17 16 frnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ⊆ 𝐾 )
18 elunii ⊢ ( ( 𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾 ) → 𝑧 ∈ ∪ 𝐾 )
19 18 1 eleqtrrdi ⊢ ( ( 𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾 ) → 𝑧 ∈ 𝑌 )
20 19 ancoms ⊢ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) → 𝑧 ∈ 𝑌 )
21 20 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → 𝑧 ∈ 𝑌 )
22 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → ran 𝐹 = 𝑌 )
23 21 22 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → 𝑧 ∈ ran 𝐹 )
24 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
25 24 1 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
26 3 25 syl ⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
27 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
28 ffn ⊢ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 → 𝐹 Fn ∪ 𝐽 )
29 fvelrnb ⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑡 ∈ ∪ 𝐽 ( 𝐹 ‘ 𝑡 ) = 𝑧 ) )
30 27 28 29 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑡 ∈ ∪ 𝐽 ( 𝐹 ‘ 𝑡 ) = 𝑧 ) )
31 23 30 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → ∃ 𝑡 ∈ ∪ 𝐽 ( 𝐹 ‘ 𝑡 ) = 𝑧 )
32 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
33 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → 𝑘 ∈ 𝐾 )
34 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑘 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑘 ) ∈ 𝐽 )
35 32 33 34 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ( ◡ 𝐹 “ 𝑘 ) ∈ 𝐽 )
36 12 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ( topGen ‘ 𝑏 ) = 𝐽 )
37 35 36 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ( ◡ 𝐹 “ 𝑘 ) ∈ ( topGen ‘ 𝑏 ) )
38 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → 𝑡 ∈ ∪ 𝐽 )
39 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ( 𝐹 ‘ 𝑡 ) = 𝑧 )
40 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → 𝑧 ∈ 𝑘 )
41 39 40 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ( 𝐹 ‘ 𝑡 ) ∈ 𝑘 )
42 27 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → 𝐹 Fn ∪ 𝐽 )
43 42 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → 𝐹 Fn ∪ 𝐽 )
44 elpreima ⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑡 ∈ ( ◡ 𝐹 “ 𝑘 ) ↔ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) ∈ 𝑘 ) ) )
45 43 44 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ( 𝑡 ∈ ( ◡ 𝐹 “ 𝑘 ) ↔ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) ∈ 𝑘 ) ) )
46 38 41 45 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → 𝑡 ∈ ( ◡ 𝐹 “ 𝑘 ) )
47 tg2 ⊢ ( ( ( ◡ 𝐹 “ 𝑘 ) ∈ ( topGen ‘ 𝑏 ) ∧ 𝑡 ∈ ( ◡ 𝐹 “ 𝑘 ) ) → ∃ 𝑚 ∈ 𝑏 ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) )
48 37 46 47 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ∃ 𝑚 ∈ 𝑏 ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) )
49 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → 𝑚 ∈ 𝑏 )
50 eqid ⊢ ( 𝐹 “ 𝑚 ) = ( 𝐹 “ 𝑚 )
51 imaeq2 ⊢ ( 𝑥 = 𝑚 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑚 ) )
52 51 rspceeqv ⊢ ( ( 𝑚 ∈ 𝑏 ∧ ( 𝐹 “ 𝑚 ) = ( 𝐹 “ 𝑚 ) ) → ∃ 𝑥 ∈ 𝑏 ( 𝐹 “ 𝑚 ) = ( 𝐹 “ 𝑥 ) )
53 49 50 52 sylancl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ∃ 𝑥 ∈ 𝑏 ( 𝐹 “ 𝑚 ) = ( 𝐹 “ 𝑥 ) )
54 43 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → 𝐹 Fn ∪ 𝐽 )
55 fnfun ⊢ ( 𝐹 Fn ∪ 𝐽 → Fun 𝐹 )
56 54 55 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → Fun 𝐹 )
57 simprrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) )
58 funimass2 ⊢ ( ( Fun 𝐹 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) → ( 𝐹 “ 𝑚 ) ⊆ 𝑘 )
59 56 57 58 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ( 𝐹 “ 𝑚 ) ⊆ 𝑘 )
60 vex ⊢ 𝑘 ∈ V
61 ssexg ⊢ ( ( ( 𝐹 “ 𝑚 ) ⊆ 𝑘 ∧ 𝑘 ∈ V ) → ( 𝐹 “ 𝑚 ) ∈ V )
62 59 60 61 sylancl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ( 𝐹 “ 𝑚 ) ∈ V )
63 eqid ⊢ ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) )
64 63 elrnmpt ⊢ ( ( 𝐹 “ 𝑚 ) ∈ V → ( ( 𝐹 “ 𝑚 ) ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝑏 ( 𝐹 “ 𝑚 ) = ( 𝐹 “ 𝑥 ) ) )
65 62 64 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ( ( 𝐹 “ 𝑚 ) ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝑏 ( 𝐹 “ 𝑚 ) = ( 𝐹 “ 𝑥 ) ) )
66 53 65 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ( 𝐹 “ 𝑚 ) ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) )
67 39 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ( 𝐹 ‘ 𝑡 ) = 𝑧 )
68 simprrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → 𝑡 ∈ 𝑚 )
69 cnvimass ⊢ ( ◡ 𝐹 “ 𝑘 ) ⊆ dom 𝐹
70 57 69 sstrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → 𝑚 ⊆ dom 𝐹 )
71 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝑚 ⊆ dom 𝐹 ) → ( 𝑡 ∈ 𝑚 → ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑚 ) ) )
72 56 70 71 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ( 𝑡 ∈ 𝑚 → ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑚 ) ) )
73 68 72 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑚 ) )
74 67 73 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → 𝑧 ∈ ( 𝐹 “ 𝑚 ) )
75 eleq2 ⊢ ( 𝑤 = ( 𝐹 “ 𝑚 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝐹 “ 𝑚 ) ) )
76 sseq1 ⊢ ( 𝑤 = ( 𝐹 “ 𝑚 ) → ( 𝑤 ⊆ 𝑘 ↔ ( 𝐹 “ 𝑚 ) ⊆ 𝑘 ) )
77 75 76 anbi12d ⊢ ( 𝑤 = ( 𝐹 “ 𝑚 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) ↔ ( 𝑧 ∈ ( 𝐹 “ 𝑚 ) ∧ ( 𝐹 “ 𝑚 ) ⊆ 𝑘 ) ) )
78 77 rspcev ⊢ ( ( ( 𝐹 “ 𝑚 ) ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ∧ ( 𝑧 ∈ ( 𝐹 “ 𝑚 ) ∧ ( 𝐹 “ 𝑚 ) ⊆ 𝑘 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) )
79 66 74 59 78 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) ∧ ( 𝑚 ∈ 𝑏 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ ( ◡ 𝐹 “ 𝑘 ) ) ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) )
80 48 79 rexlimddv ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) )
81 80 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) ∧ ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑧 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) )
82 31 81 rexlimddv ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) )
83 82 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ∀ 𝑘 ∈ 𝐾 ∀ 𝑧 ∈ 𝑘 ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) )
84 basgen2 ⊢ ( ( 𝐾 ∈ Top ∧ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ⊆ 𝐾 ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑧 ∈ 𝑘 ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ) = 𝐾 )
85 8 17 83 84 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ) = 𝐾 )
86 85 8 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ) ∈ Top )
87 tgclb ⊢ ( ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ∈ TopBases ↔ ( topGen ‘ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ) ∈ Top )
88 86 87 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ∈ TopBases )
89 omelon ⊢ ω ∈ On
90 simprl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → 𝑏 ≼ ω )
91 ondomen ⊢ ( ( ω ∈ On ∧ 𝑏 ≼ ω ) → 𝑏 ∈ dom card )
92 89 90 91 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → 𝑏 ∈ dom card )
93 16 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) Fn 𝑏 )
94 dffn4 ⊢ ( ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) Fn 𝑏 ↔ ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) : 𝑏 –onto→ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) )
95 93 94 sylib ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) : 𝑏 –onto→ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) )
96 fodomnum ⊢ ( 𝑏 ∈ dom card → ( ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) : 𝑏 –onto→ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) → ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ≼ 𝑏 ) )
97 92 95 96 sylc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ≼ 𝑏 )
98 domtr ⊢ ( ( ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ≼ 𝑏 ∧ 𝑏 ≼ ω ) → ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ≼ ω )
99 97 90 98 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ≼ ω )
100 2ndci ⊢ ( ( ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ∈ TopBases ∧ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ) ∈ 2ndω )
101 88 99 100 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑏 ↦ ( 𝐹 “ 𝑥 ) ) ) ∈ 2ndω )
102 85 101 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → 𝐾 ∈ 2ndω )
103 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) )
104 2 103 sylib ⊢ ( 𝜑 → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) )
105 102 104 r19.29a ⊢ ( 𝜑 → 𝐾 ∈ 2ndω )