Metamath Proof Explorer


Theorem opnreen

Description: Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 20-Feb-2015)

Ref Expression
Assertion opnreen ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ 𝐴 β‰  βˆ… ) β†’ 𝐴 β‰ˆ 𝒫 β„• )

Proof

Step Hyp Ref Expression
1 reex ⊒ ℝ ∈ V
2 elssuni ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ 𝐴 βŠ† βˆͺ ( topGen β€˜ ran (,) ) )
3 uniretop ⊒ ℝ = βˆͺ ( topGen β€˜ ran (,) )
4 2 3 sseqtrrdi ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ 𝐴 βŠ† ℝ )
5 ssdomg ⊒ ( ℝ ∈ V β†’ ( 𝐴 βŠ† ℝ β†’ 𝐴 β‰Ό ℝ ) )
6 1 4 5 mpsyl ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ 𝐴 β‰Ό ℝ )
7 rpnnen ⊒ ℝ β‰ˆ 𝒫 β„•
8 domentr ⊒ ( ( 𝐴 β‰Ό ℝ ∧ ℝ β‰ˆ 𝒫 β„• ) β†’ 𝐴 β‰Ό 𝒫 β„• )
9 6 7 8 sylancl ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ 𝐴 β‰Ό 𝒫 β„• )
10 n0 ⊒ ( 𝐴 β‰  βˆ… ↔ βˆƒ π‘₯ π‘₯ ∈ 𝐴 )
11 4 sselda ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ π‘₯ ∈ ℝ )
12 rpnnen2 ⊒ 𝒫 β„• β‰Ό ( 0 [,] 1 )
13 rphalfcl ⊒ ( 𝑦 ∈ ℝ+ β†’ ( 𝑦 / 2 ) ∈ ℝ+ )
14 13 rpred ⊒ ( 𝑦 ∈ ℝ+ β†’ ( 𝑦 / 2 ) ∈ ℝ )
15 resubcl ⊒ ( ( π‘₯ ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) β†’ ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) ∈ ℝ )
16 14 15 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) ∈ ℝ )
17 readdcl ⊒ ( ( π‘₯ ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) β†’ ( π‘₯ + ( 𝑦 / 2 ) ) ∈ ℝ )
18 14 17 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ + ( 𝑦 / 2 ) ) ∈ ℝ )
19 simpl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ π‘₯ ∈ ℝ )
20 ltsubrp ⊒ ( ( π‘₯ ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) < π‘₯ )
21 13 20 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) < π‘₯ )
22 ltaddrp ⊒ ( ( π‘₯ ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) β†’ π‘₯ < ( π‘₯ + ( 𝑦 / 2 ) ) )
23 13 22 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ π‘₯ < ( π‘₯ + ( 𝑦 / 2 ) ) )
24 16 19 18 21 23 lttrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) < ( π‘₯ + ( 𝑦 / 2 ) ) )
25 iccen ⊒ ( ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) ∈ ℝ ∧ ( π‘₯ + ( 𝑦 / 2 ) ) ∈ ℝ ∧ ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) < ( π‘₯ + ( 𝑦 / 2 ) ) ) β†’ ( 0 [,] 1 ) β‰ˆ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) )
26 16 18 24 25 syl3anc ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( 0 [,] 1 ) β‰ˆ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) )
27 domentr ⊒ ( ( 𝒫 β„• β‰Ό ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) β‰ˆ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) ) β†’ 𝒫 β„• β‰Ό ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) )
28 12 26 27 sylancr ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ 𝒫 β„• β‰Ό ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) )
29 ovex ⊒ ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) ∈ V
30 rpre ⊒ ( 𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ )
31 resubcl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( π‘₯ βˆ’ 𝑦 ) ∈ ℝ )
32 30 31 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ 𝑦 ) ∈ ℝ )
33 32 rexrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ 𝑦 ) ∈ ℝ* )
34 readdcl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( π‘₯ + 𝑦 ) ∈ ℝ )
35 30 34 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ + 𝑦 ) ∈ ℝ )
36 35 rexrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ + 𝑦 ) ∈ ℝ* )
37 19 recnd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ π‘₯ ∈ β„‚ )
38 14 adantl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( 𝑦 / 2 ) ∈ ℝ )
39 38 recnd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( 𝑦 / 2 ) ∈ β„‚ )
40 37 39 39 subsub4d ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) βˆ’ ( 𝑦 / 2 ) ) = ( π‘₯ βˆ’ ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
41 30 adantl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ 𝑦 ∈ ℝ )
42 41 recnd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ 𝑦 ∈ β„‚ )
43 42 2halvesd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
44 43 oveq2d ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( π‘₯ βˆ’ 𝑦 ) )
45 40 44 eqtrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) βˆ’ ( 𝑦 / 2 ) ) = ( π‘₯ βˆ’ 𝑦 ) )
46 13 adantl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( 𝑦 / 2 ) ∈ ℝ+ )
47 16 46 ltsubrpd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) βˆ’ ( 𝑦 / 2 ) ) < ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) )
48 45 47 eqbrtrrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ βˆ’ 𝑦 ) < ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) )
49 18 46 ltaddrpd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ + ( 𝑦 / 2 ) ) < ( ( π‘₯ + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
50 37 39 39 addassd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( π‘₯ + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( π‘₯ + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
51 43 oveq2d ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( π‘₯ + 𝑦 ) )
52 50 51 eqtrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( π‘₯ + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( π‘₯ + 𝑦 ) )
53 49 52 breqtrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ + ( 𝑦 / 2 ) ) < ( π‘₯ + 𝑦 ) )
54 iccssioo ⊒ ( ( ( ( π‘₯ βˆ’ 𝑦 ) ∈ ℝ* ∧ ( π‘₯ + 𝑦 ) ∈ ℝ* ) ∧ ( ( π‘₯ βˆ’ 𝑦 ) < ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) ∧ ( π‘₯ + ( 𝑦 / 2 ) ) < ( π‘₯ + 𝑦 ) ) ) β†’ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) βŠ† ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) )
55 33 36 48 53 54 syl22anc ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) βŠ† ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) )
56 ssdomg ⊒ ( ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) ∈ V β†’ ( ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) βŠ† ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) β†’ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) β‰Ό ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) ) )
57 29 55 56 mpsyl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) β‰Ό ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) )
58 domtr ⊒ ( ( 𝒫 β„• β‰Ό ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) ∧ ( ( π‘₯ βˆ’ ( 𝑦 / 2 ) ) [,] ( π‘₯ + ( 𝑦 / 2 ) ) ) β‰Ό ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) ) β†’ 𝒫 β„• β‰Ό ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) )
59 28 57 58 syl2anc ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ 𝒫 β„• β‰Ό ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) )
60 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
61 60 bl2ioo ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) = ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) )
62 30 61 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) = ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) )
63 59 62 breqtrrd ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) β†’ 𝒫 β„• β‰Ό ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) )
64 11 63 sylan ⊒ ( ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) β†’ 𝒫 β„• β‰Ό ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) )
65 simplll ⊒ ( ( ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 ) β†’ 𝐴 ∈ ( topGen β€˜ ran (,) ) )
66 simpr ⊒ ( ( ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 ) β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 )
67 ssdomg ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ ( ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) β‰Ό 𝐴 ) )
68 65 66 67 sylc ⊒ ( ( ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 ) β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) β‰Ό 𝐴 )
69 domtr ⊒ ( ( 𝒫 β„• β‰Ό ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) β‰Ό 𝐴 ) β†’ 𝒫 β„• β‰Ό 𝐴 )
70 64 68 69 syl2an2r ⊒ ( ( ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 ) β†’ 𝒫 β„• β‰Ό 𝐴 )
71 eqid ⊒ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
72 60 71 tgioo ⊒ ( topGen β€˜ ran (,) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
73 72 eleq2i ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ↔ 𝐴 ∈ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) )
74 60 rexmet ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ )
75 71 mopni2 ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ 𝐴 ∈ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) ∧ π‘₯ ∈ 𝐴 ) β†’ βˆƒ 𝑦 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 )
76 74 75 mp3an1 ⊒ ( ( 𝐴 ∈ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) ∧ π‘₯ ∈ 𝐴 ) β†’ βˆƒ 𝑦 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 )
77 73 76 sylanb ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ βˆƒ 𝑦 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑦 ) βŠ† 𝐴 )
78 70 77 r19.29a ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ 𝒫 β„• β‰Ό 𝐴 )
79 78 ex ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ ( π‘₯ ∈ 𝐴 β†’ 𝒫 β„• β‰Ό 𝐴 ) )
80 79 exlimdv ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ ( βˆƒ π‘₯ π‘₯ ∈ 𝐴 β†’ 𝒫 β„• β‰Ό 𝐴 ) )
81 10 80 biimtrid ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ ( 𝐴 β‰  βˆ… β†’ 𝒫 β„• β‰Ό 𝐴 ) )
82 81 imp ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ 𝐴 β‰  βˆ… ) β†’ 𝒫 β„• β‰Ό 𝐴 )
83 sbth ⊒ ( ( 𝐴 β‰Ό 𝒫 β„• ∧ 𝒫 β„• β‰Ό 𝐴 ) β†’ 𝐴 β‰ˆ 𝒫 β„• )
84 9 82 83 syl2an2r ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ 𝐴 β‰  βˆ… ) β†’ 𝐴 β‰ˆ 𝒫 β„• )