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 
|- ( ( J e. 2ndc /\ A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om )

Proof

Step Hyp Ref Expression
1 is2ndc 
 |-  ( J e. 2ndc <-> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) )
2 omex 
 |-  _om e. _V
3 2 brdom 
 |-  ( b ~<_ _om <-> E. f f : b -1-1-> _om )
4 ssrab2 
 |-  { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ ran f
5 f1f 
 |-  ( f : b -1-1-> _om -> f : b --> _om )
6 5 frnd 
 |-  ( f : b -1-1-> _om -> ran f C_ _om )
7 6 adantl 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ran f C_ _om )
8 4 7 sstrid 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ _om )
9 8 adantr 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) -> { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ _om )
10 eldifsn 
 |-  ( B e. ( ( topGen ` b ) \ { (/) } ) <-> ( B e. ( topGen ` b ) /\ B =/= (/) ) )
11 n0 
 |-  ( B =/= (/) <-> E. y y e. B )
12 tg2 
 |-  ( ( B e. ( topGen ` b ) /\ y e. B ) -> E. z e. b ( y e. z /\ z C_ B ) )
13 omsson 
 |-  _om C_ On
14 8 13 sstrdi 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ On )
15 14 ad2antrr 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ On )
16 f1fn 
 |-  ( f : b -1-1-> _om -> f Fn b )
17 16 ad3antlr 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> f Fn b )
18 simprl 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z e. b )
19 fnfvelrn 
 |-  ( ( f Fn b /\ z e. b ) -> ( f ` z ) e. ran f )
20 17 18 19 syl2anc 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> ( f ` z ) e. ran f )
21 f1f1orn 
 |-  ( f : b -1-1-> _om -> f : b -1-1-onto-> ran f )
22 21 ad3antlr 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> f : b -1-1-onto-> ran f )
23 f1ocnvfv1 
 |-  ( ( f : b -1-1-onto-> ran f /\ z e. b ) -> ( `' f ` ( f ` z ) ) = z )
24 22 18 23 syl2anc 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> ( `' f ` ( f ` z ) ) = z )
25 simprrr 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z C_ B )
26 velpw 
 |-  ( z e. ~P B <-> z C_ B )
27 25 26 sylibr 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z e. ~P B )
28 simprrl 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> y e. z )
29 28 ne0d 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z =/= (/) )
30 eldifsn 
 |-  ( z e. ( ~P B \ { (/) } ) <-> ( z e. ~P B /\ z =/= (/) ) )
31 27 29 30 sylanbrc 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z e. ( ~P B \ { (/) } ) )
32 24 31 eqeltrd 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> ( `' f ` ( f ` z ) ) e. ( ~P B \ { (/) } ) )
33 fveq2 
 |-  ( n = ( f ` z ) -> ( `' f ` n ) = ( `' f ` ( f ` z ) ) )
34 33 eleq1d 
 |-  ( n = ( f ` z ) -> ( ( `' f ` n ) e. ( ~P B \ { (/) } ) <-> ( `' f ` ( f ` z ) ) e. ( ~P B \ { (/) } ) ) )
35 34 rspcev 
 |-  ( ( ( f ` z ) e. ran f /\ ( `' f ` ( f ` z ) ) e. ( ~P B \ { (/) } ) ) -> E. n e. ran f ( `' f ` n ) e. ( ~P B \ { (/) } ) )
36 20 32 35 syl2anc 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> E. n e. ran f ( `' f ` n ) e. ( ~P B \ { (/) } ) )
37 rabn0 
 |-  ( { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } =/= (/) <-> E. n e. ran f ( `' f ` n ) e. ( ~P B \ { (/) } ) )
38 36 37 sylibr 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } =/= (/) )
39 onint 
 |-  ( ( { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ On /\ { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } =/= (/) ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
40 15 38 39 syl2anc 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
41 40 rexlimdvaa 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) -> ( E. z e. b ( y e. z /\ z C_ B ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
42 12 41 syl5 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) -> ( ( B e. ( topGen ` b ) /\ y e. B ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
43 42 expdimp 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ B e. ( topGen ` b ) ) -> ( y e. B -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
44 43 exlimdv 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ B e. ( topGen ` b ) ) -> ( E. y y e. B -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
45 11 44 biimtrid 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) /\ B e. ( topGen ` b ) ) -> ( B =/= (/) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
46 45 expimpd 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) -> ( ( B e. ( topGen ` b ) /\ B =/= (/) ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
47 10 46 biimtrid 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) -> ( B e. ( ( topGen ` b ) \ { (/) } ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
48 47 impr 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
49 9 48 sseldd 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. _om )
50 49 expr 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ x e. A ) -> ( B e. ( ( topGen ` b ) \ { (/) } ) -> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. _om ) )
51 50 ralimdva 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) -> A. x e. A |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. _om ) )
52 51 imp 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) ) -> A. x e. A |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. _om )
53 52 adantrr 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) ) -> A. x e. A |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. _om )
54 eqid 
 |-  ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) = ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
55 54 fmpt 
 |-  ( A. x e. A |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. _om <-> ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) : A --> _om )
56 53 55 sylib 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) ) -> ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) : A --> _om )
57 neeq1 
 |-  ( ( `' f ` z ) = if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> ( ( `' f ` z ) =/= (/) <-> if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/) ) )
58 neeq1 
 |-  ( 1o = if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> ( 1o =/= (/) <-> if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/) ) )
59 1n0 
 |-  1o =/= (/)
60 57 58 59 elimhyp 
 |-  if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/)
61 n0 
 |-  ( if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/) <-> E. y y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) )
62 60 61 mpbi 
 |-  E. y y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o )
63 19.29r 
 |-  ( ( E. y y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) /\ A. y E* x e. A y e. B ) -> E. y ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) /\ E* x e. A y e. B ) )
64 62 63 mpan 
 |-  ( A. y E* x e. A y e. B -> E. y ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) /\ E* x e. A y e. B ) )
65 eleq1 
 |-  ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> ( z e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } <-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
66 48 65 syl5ibrcom 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) -> ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> z e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
67 66 imp 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> z e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
68 fveq2 
 |-  ( n = z -> ( `' f ` n ) = ( `' f ` z ) )
69 68 eleq1d 
 |-  ( n = z -> ( ( `' f ` n ) e. ( ~P B \ { (/) } ) <-> ( `' f ` z ) e. ( ~P B \ { (/) } ) ) )
70 69 elrab 
 |-  ( z e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } <-> ( z e. ran f /\ ( `' f ` z ) e. ( ~P B \ { (/) } ) ) )
71 70 simprbi 
 |-  ( z e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> ( `' f ` z ) e. ( ~P B \ { (/) } ) )
72 67 71 syl 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> ( `' f ` z ) e. ( ~P B \ { (/) } ) )
73 eldifsn 
 |-  ( ( `' f ` z ) e. ( ~P B \ { (/) } ) <-> ( ( `' f ` z ) e. ~P B /\ ( `' f ` z ) =/= (/) ) )
74 72 73 sylib 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> ( ( `' f ` z ) e. ~P B /\ ( `' f ` z ) =/= (/) ) )
75 74 simprd 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> ( `' f ` z ) =/= (/) )
76 75 iftrued 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) = ( `' f ` z ) )
77 74 simpld 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> ( `' f ` z ) e. ~P B )
78 77 elpwid 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> ( `' f ` z ) C_ B )
79 76 78 eqsstrd 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) C_ B )
80 79 sseld 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) ) /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) -> ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> y e. B ) )
81 80 exp31 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ( ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) -> ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> y e. B ) ) ) )
82 81 com23 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> ( ( x e. A /\ B e. ( ( topGen ` b ) \ { (/) } ) ) -> ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> y e. B ) ) ) )
83 82 exp4a 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> ( x e. A -> ( B e. ( ( topGen ` b ) \ { (/) } ) -> ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> y e. B ) ) ) ) )
84 83 com25 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> ( x e. A -> ( B e. ( ( topGen ` b ) \ { (/) } ) -> ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> y e. B ) ) ) ) )
85 84 imp31 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) ) /\ x e. A ) -> ( B e. ( ( topGen ` b ) \ { (/) } ) -> ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> y e. B ) ) )
86 85 ralimdva 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) ) -> ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) -> A. x e. A ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> y e. B ) ) )
87 86 imp 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) ) /\ A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) ) -> A. x e. A ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> y e. B ) )
88 87 an32s 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) ) /\ y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) ) -> A. x e. A ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> y e. B ) )
89 rmoim 
 |-  ( A. x e. A ( z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> y e. B ) -> ( E* x e. A y e. B -> E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
90 88 89 syl 
 |-  ( ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) ) /\ y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) ) -> ( E* x e. A y e. B -> E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
91 90 expimpd 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) ) -> ( ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) /\ E* x e. A y e. B ) -> E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
92 91 exlimdv 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) ) -> ( E. y ( y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) /\ E* x e. A y e. B ) -> E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
93 64 92 syl5 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) ) -> ( A. y E* x e. A y e. B -> E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
94 93 impr 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) ) -> E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
95 nfcv 
 |-  F/_ x w
96 nfmpt1 
 |-  F/_ x ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
97 nfcv 
 |-  F/_ x z
98 95 96 97 nfbr 
 |-  F/ x w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z
99 nfv 
 |-  F/ w ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
100 breq1 
 |-  ( w = x -> ( w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z <-> x ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z ) )
101 df-br 
 |-  ( x ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z <-> <. x , z >. e. ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
102 df-mpt 
 |-  ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) = { <. x , z >. | ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) }
103 102 eleq2i 
 |-  ( <. x , z >. e. ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) <-> <. x , z >. e. { <. x , z >. | ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) } )
104 opabidw 
 |-  ( <. x , z >. e. { <. x , z >. | ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) } <-> ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
105 101 103 104 3bitri 
 |-  ( x ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z <-> ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
106 100 105 bitrdi 
 |-  ( w = x -> ( w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z <-> ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) ) )
107 98 99 106 cbvmow 
 |-  ( E* w w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z <-> E* x ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
108 df-rmo 
 |-  ( E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } <-> E* x ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) )
109 107 108 bitr4i 
 |-  ( E* w w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z <-> E* x e. A z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
110 94 109 sylibr 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) ) -> E* w w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z )
111 110 alrimiv 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) ) -> A. z E* w w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z )
112 dff12 
 |-  ( ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) : A -1-1-> _om <-> ( ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) : A --> _om /\ A. z E* w w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z ) )
113 56 111 112 sylanbrc 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) ) -> ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) : A -1-1-> _om )
114 f1domg 
 |-  ( _om e. _V -> ( ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) : A -1-1-> _om -> A ~<_ _om ) )
115 2 113 114 mpsyl 
 |-  ( ( ( b e. TopBases /\ f : b -1-1-> _om ) /\ ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) ) -> A ~<_ _om )
116 115 ex 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ( ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) )
117 difeq1 
 |-  ( ( topGen ` b ) = J -> ( ( topGen ` b ) \ { (/) } ) = ( J \ { (/) } ) )
118 117 eleq2d 
 |-  ( ( topGen ` b ) = J -> ( B e. ( ( topGen ` b ) \ { (/) } ) <-> B e. ( J \ { (/) } ) ) )
119 118 ralbidv 
 |-  ( ( topGen ` b ) = J -> ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) <-> A. x e. A B e. ( J \ { (/) } ) ) )
120 119 anbi1d 
 |-  ( ( topGen ` b ) = J -> ( ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) <-> ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) ) )
121 120 imbi1d 
 |-  ( ( topGen ` b ) = J -> ( ( ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) <-> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) ) )
122 116 121 syl5ibcom 
 |-  ( ( b e. TopBases /\ f : b -1-1-> _om ) -> ( ( topGen ` b ) = J -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) ) )
123 122 ex 
 |-  ( b e. TopBases -> ( f : b -1-1-> _om -> ( ( topGen ` b ) = J -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) ) ) )
124 123 exlimdv 
 |-  ( b e. TopBases -> ( E. f f : b -1-1-> _om -> ( ( topGen ` b ) = J -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) ) ) )
125 3 124 biimtrid 
 |-  ( b e. TopBases -> ( b ~<_ _om -> ( ( topGen ` b ) = J -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) ) ) )
126 125 impd 
 |-  ( b e. TopBases -> ( ( b ~<_ _om /\ ( topGen ` b ) = J ) -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) ) )
127 126 rexlimiv 
 |-  ( E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) )
128 1 127 sylbi 
 |-  ( J e. 2ndc -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om ) )
129 128 3impib 
 |-  ( ( J e. 2ndc /\ A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ _om )