Metamath Proof Explorer

Theorem 2ndcdisj

Description: Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015) (Proof shortened by Mario Carneiro, 9-Apr-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion 2ndcdisj ( ( 𝐽 ∈ 2ndω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω )

Proof

Step Hyp Ref Expression
1 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) )
2 omex ⊢ ω ∈ V
3 2 brdom ⊢ ( 𝑏 ≼ ω ↔ ∃ 𝑓 𝑓 : 𝑏 –1-1→ ω )
4 ssrab2 ⊢ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ⊆ ran 𝑓
5 f1f ⊢ ( 𝑓 : 𝑏 –1-1→ ω → 𝑓 : 𝑏 ⟶ ω )
6 5 frnd ⊢ ( 𝑓 : 𝑏 –1-1→ ω → ran 𝑓 ⊆ ω )
7 6 adantl ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ran 𝑓 ⊆ ω )
8 4 7 sstrid ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ⊆ ω )
9 8 adantr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) → { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ⊆ ω )
10 eldifsn ⊢ ( 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ↔ ( 𝐵 ∈ ( topGen ‘ 𝑏 ) ∧ 𝐵 ≠ ∅ ) )
11 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
12 tg2 ⊢ ( ( 𝐵 ∈ ( topGen ‘ 𝑏 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝑏 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) )
13 omsson ⊢ ω ⊆ On
14 8 13 sstrdi ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ⊆ On )
15 14 ad2antrr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ⊆ On )
16 f1fn ⊢ ( 𝑓 : 𝑏 –1-1→ ω → 𝑓 Fn 𝑏 )
17 16 ad3antlr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑓 Fn 𝑏 )
18 simprl ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑧 ∈ 𝑏 )
19 fnfvelrn ⊢ ( ( 𝑓 Fn 𝑏 ∧ 𝑧 ∈ 𝑏 ) → ( 𝑓 ‘ 𝑧 ) ∈ ran 𝑓 )
20 17 18 19 syl2anc ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑧 ) ∈ ran 𝑓 )
21 f1f1orn ⊢ ( 𝑓 : 𝑏 –1-1→ ω → 𝑓 : 𝑏 –1-1-onto→ ran 𝑓 )
22 21 ad3antlr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑓 : 𝑏 –1-1-onto→ ran 𝑓 )
23 f1ocnvfv1 ⊢ ( ( 𝑓 : 𝑏 –1-1-onto→ ran 𝑓 ∧ 𝑧 ∈ 𝑏 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) = 𝑧 )
24 22 18 23 syl2anc ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) = 𝑧 )
25 simprrr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑧 ⊆ 𝐵 )
26 velpw ⊢ ( 𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵 )
27 25 26 sylibr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑧 ∈ 𝒫 𝐵 )
28 simprrl ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑦 ∈ 𝑧 )
29 28 ne0d ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑧 ≠ ∅ )
30 eldifsn ⊢ ( 𝑧 ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ↔ ( 𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ≠ ∅ ) )
31 27 29 30 sylanbrc ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → 𝑧 ∈ ( 𝒫 𝐵 ∖ { ∅ } ) )
32 24 31 eqeltrd ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) )
33 fveq2 ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑧 ) → ( ◡ 𝑓 ‘ 𝑛 ) = ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) )
34 33 eleq1d ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑧 ) → ( ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ↔ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ) )
35 34 rspcev ⊢ ( ( ( 𝑓 ‘ 𝑧 ) ∈ ran 𝑓 ∧ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ) → ∃ 𝑛 ∈ ran 𝑓 ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) )
36 20 32 35 syl2anc ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → ∃ 𝑛 ∈ ran 𝑓 ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) )
37 rabn0 ⊢ ( { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ≠ ∅ ↔ ∃ 𝑛 ∈ ran 𝑓 ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) )
38 36 37 sylibr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ≠ ∅ )
39 onint ⊢ ( ( { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ⊆ On ∧ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ≠ ∅ ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
40 15 38 39 syl2anc ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑏 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) ) ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
41 40 rexlimdvaa ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝑏 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
42 12 41 syl5 ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ∈ ( topGen ‘ 𝑏 ) ∧ 𝑦 ∈ 𝐵 ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
43 42 expdimp ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ∈ ( topGen ‘ 𝑏 ) ) → ( 𝑦 ∈ 𝐵 → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
44 43 exlimdv ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ∈ ( topGen ‘ 𝑏 ) ) → ( ∃ 𝑦 𝑦 ∈ 𝐵 → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
45 11 44 syl5bi ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ∈ ( topGen ‘ 𝑏 ) ) → ( 𝐵 ≠ ∅ → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
46 45 expimpd ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ∈ ( topGen ‘ 𝑏 ) ∧ 𝐵 ≠ ∅ ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
47 10 46 syl5bi ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
48 47 impr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
49 9 48 sseldd ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ ω )
50 49 expr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) → ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ ω ) )
51 50 ralimdva ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) → ∀ 𝑥 ∈ 𝐴 ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ ω ) )
52 51 imp ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) → ∀ 𝑥 ∈ 𝐴 ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ ω )
53 52 adantrr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ ω )
54 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) = ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
55 54 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ ω ↔ ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) : 𝐴 ⟶ ω )
56 53 55 sylib ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) : 𝐴 ⟶ ω )
57 neeq1 ⊢ ( ( ◡ 𝑓 ‘ 𝑧 ) = if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) → ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ ↔ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ≠ ∅ ) )
58 neeq1 ⊢ ( 1o = if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) → ( 1o ≠ ∅ ↔ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ≠ ∅ ) )
59 1n0 ⊢ 1o ≠ ∅
60 57 58 59 elimhyp ⊢ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ≠ ∅
61 n0 ⊢ ( if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) )
62 60 61 mpbi ⊢ ∃ 𝑦 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o )
63 19.29r ⊢ ( ( ∃ 𝑦 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ∃ 𝑦 ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ∧ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
64 62 63 mpan ⊢ ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃ 𝑦 ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ∧ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
65 eleq1 ⊢ ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → ( 𝑧 ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ↔ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
66 48 65 syl5ibrcom ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) → ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → 𝑧 ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
67 66 imp ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → 𝑧 ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
68 fveq2 ⊢ ( 𝑛 = 𝑧 → ( ◡ 𝑓 ‘ 𝑛 ) = ( ◡ 𝑓 ‘ 𝑧 ) )
69 68 eleq1d ⊢ ( 𝑛 = 𝑧 → ( ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ↔ ( ◡ 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ) )
70 69 elrab ⊢ ( 𝑧 ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ↔ ( 𝑧 ∈ ran 𝑓 ∧ ( ◡ 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ) )
71 70 simprbi ⊢ ( 𝑧 ∈ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → ( ◡ 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) )
72 67 71 syl ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → ( ◡ 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) )
73 eldifsn ⊢ ( ( ◡ 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) ↔ ( ( ◡ 𝑓 ‘ 𝑧 ) ∈ 𝒫 𝐵 ∧ ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ ) )
74 72 73 sylib ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → ( ( ◡ 𝑓 ‘ 𝑧 ) ∈ 𝒫 𝐵 ∧ ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ ) )
75 74 simprd ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ )
76 75 iftrued ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) = ( ◡ 𝑓 ‘ 𝑧 ) )
77 74 simpld ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → ( ◡ 𝑓 ‘ 𝑧 ) ∈ 𝒫 𝐵 )
78 77 elpwid ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → ( ◡ 𝑓 ‘ 𝑧 ) ⊆ 𝐵 )
79 76 78 eqsstrd ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ⊆ 𝐵 )
80 79 sseld ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ) ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) → ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) → 𝑦 ∈ 𝐵 ) )
81 80 exp31 ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) → ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) → 𝑦 ∈ 𝐵 ) ) ) )
82 81 com23 ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) → ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) → 𝑦 ∈ 𝐵 ) ) ) )
83 82 exp4a ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) → ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) → 𝑦 ∈ 𝐵 ) ) ) ) )
84 83 com25 ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) → ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → 𝑦 ∈ 𝐵 ) ) ) ) )
85 84 imp31 ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) → ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → 𝑦 ∈ 𝐵 ) ) )
86 85 ralimdva ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) → ∀ 𝑥 ∈ 𝐴 ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → 𝑦 ∈ 𝐵 ) ) )
87 86 imp ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → 𝑦 ∈ 𝐵 ) )
88 87 an32s ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ∧ 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → 𝑦 ∈ 𝐵 ) )
89 rmoim ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } → 𝑦 ∈ 𝐵 ) → ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
90 88 89 syl ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) ∧ 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ) → ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
91 90 expimpd ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) → ( ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ∧ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
92 91 exlimdv ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) → ( ∃ 𝑦 ( 𝑦 ∈ if ( ( ◡ 𝑓 ‘ 𝑧 ) ≠ ∅ , ( ◡ 𝑓 ‘ 𝑧 ) , 1o ) ∧ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
93 64 92 syl5 ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ) → ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
94 93 impr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) → ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
95 nfcv ⊢ Ⅎ 𝑥 𝑤
96 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
97 nfcv ⊢ Ⅎ 𝑥 𝑧
98 95 96 97 nfbr ⊢ Ⅎ 𝑥 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧
99 nfv ⊢ Ⅎ 𝑤 ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
100 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ↔ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ) )
101 df-br ⊢ ( 𝑥 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
102 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) }
103 102 eleq2i ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) } )
104 opabidw ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
105 101 103 104 3bitri ⊢ ( 𝑥 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
106 100 105 bitrdi ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) ) )
107 98 99 106 cbvmow ⊢ ( ∃* 𝑤 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
108 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) )
109 107 108 bitr4i ⊢ ( ∃* 𝑤 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ↔ ∃* 𝑥 ∈ 𝐴 𝑧 = ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } )
110 94 109 sylibr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) → ∃* 𝑤 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 )
111 110 alrimiv ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) → ∀ 𝑧 ∃* 𝑤 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 )
112 dff12 ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) : 𝐴 –1-1→ ω ↔ ( ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) : 𝐴 ⟶ ω ∧ ∀ 𝑧 ∃* 𝑤 𝑤 ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) 𝑧 ) )
113 56 111 112 sylanbrc ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) : 𝐴 –1-1→ ω )
114 f1domg ⊢ ( ω ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ ∩ { 𝑛 ∈ ran 𝑓 ∣ ( ◡ 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 𝐵 ∖ { ∅ } ) } ) : 𝐴 –1-1→ ω → 𝐴 ≼ ω ) )
115 2 113 114 mpsyl ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) → 𝐴 ≼ ω )
116 115 ex ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) )
117 difeq1 ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) = ( 𝐽 ∖ { ∅ } ) )
118 117 eleq2d ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ↔ 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ) )
119 118 ralbidv ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ) )
120 119 anbi1d ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) )
121 120 imbi1d ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( ( topGen ‘ 𝑏 ) ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) ) )
122 116 121 syl5ibcom ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑓 : 𝑏 –1-1→ ω ) → ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) ) )
123 122 ex ⊢ ( 𝑏 ∈ TopBases → ( 𝑓 : 𝑏 –1-1→ ω → ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) ) ) )
124 123 exlimdv ⊢ ( 𝑏 ∈ TopBases → ( ∃ 𝑓 𝑓 : 𝑏 –1-1→ ω → ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) ) ) )
125 3 124 syl5bi ⊢ ( 𝑏 ∈ TopBases → ( 𝑏 ≼ ω → ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) ) ) )
126 125 impd ⊢ ( 𝑏 ∈ TopBases → ( ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) ) )
127 126 rexlimiv ⊢ ( ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) )
128 1 127 sylbi ⊢ ( 𝐽 ∈ 2ndω → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω ) )
129 128 3impib ⊢ ( ( 𝐽 ∈ 2ndω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝐴 ≼ ω )