MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2ndcdisj Structured version   Unicode version
Theorem 2ndcdisj 18960
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.)
Assertion
Ref Expression
2ndcdisj |- ( ( J e. 2ndc /\ A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ om )
Distinct variable groups:   x, y, A   y, B   x, J
Allowed substitution hints:   B( x)   J( y)
Proof of Theorem 2ndcdisj
Dummy variables f b w z n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 is2ndc 18950 . . 3 |- ( J e. 2ndc <-> E. b e. TopBases ( b ~<_ om /\ ( topGen ` b ) = J ) )
2 omex 7845 . . . . . . 7 |- om e. _V
32brdom 7318 . . . . . 6 |- ( b ~<_ om <-> E. f f : b -1-1-> om )
4 ssrab2 3434 . . . . . . . . . . . . . . . . . . . 20 |- { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ ran f
5 f1f 5603 . . . . . . . . . . . . . . . . . . . . . 22 |- ( f : b -1-1-> om -> f : b --> om )
6 frn 5562 . . . . . . . . . . . . . . . . . . . . . 22 |- ( f : b --> om -> ran f C_ om )
75, 6syl 16 . . . . . . . . . . . . . . . . . . . . 21 |- ( f : b -1-1-> om -> ran f C_ om )
87adantl 463 . . . . . . . . . . . . . . . . . . . 20 |- ( ( b e. TopBases /\ f : b -1-1-> om ) -> ran f C_ om )
94, 8syl5ss 3364 . . . . . . . . . . . . . . . . . . 19 |- ( ( b e. TopBases /\ f : b -1-1-> om ) -> { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ om )
109adantr 462 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 )
11 eldifsn 3997 . . . . . . . . . . . . . . . . . . . 20 |- ( B e. ( ( topGen ` b ) \ { (/) } ) <-> ( B e. ( topGen ` b ) /\ B =/= (/) ) )
12 n0 3643 . . . . . . . . . . . . . . . . . . . . . 22 |- ( B =/= (/) <-> E. y y e. B )
13 tg2 18470 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( B e. ( topGen ` b ) /\ y e. B ) -> E. z e. b ( y e. z /\ z C_ B ) )
14 omsson 6479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- om C_ On
159, 14syl6ss 3365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( b e. TopBases /\ f : b -1-1-> om ) -> { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } C_ On )
1615ad2antrr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 )
17 f1fn 5604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f : b -1-1-> om -> f Fn b )
1817ad3antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> f Fn b )
19 simprl 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z e. b )
20 fnfvelrn 5837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( f Fn b /\ z e. b ) -> ( f ` z ) e. ran f )
2118, 19, 20syl2anc 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 )
22 f1f1orn 5649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f : b -1-1-> om -> f : b -1-1-onto-> ran f )
2322ad3antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( 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 )
24 f1ocnvfv1 5980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( f : b -1-1-onto-> ran f /\ z e. b ) -> ( `' f ` ( f ` z ) ) = z )
2523, 19, 24syl2anc 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> ( `' f ` ( f ` z ) ) = z )
26 simprrr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z C_ B )
27 selpw 3864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z e. ~P B <-> z C_ B )
2826, 27sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z e. ~P B )
29 simprrl 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> y e. z )
30 ne0i 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y e. z -> z =/= (/) )
3129, 30syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z =/= (/) )
32 eldifsn 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z e. ( ~P B \ { (/) } ) <-> ( z e. ~P B /\ z =/= (/) ) )
3328, 31, 32sylanbrc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( b e. TopBases /\ f : b -1-1-> om ) /\ x e. A ) /\ ( z e. b /\ ( y e. z /\ z C_ B ) ) ) -> z e. ( ~P B \ { (/) } ) )
3425, 33eqeltrd 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 \ { (/) } ) )
35 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = ( f ` z ) -> ( `' f ` n ) = ( `' f ` ( f ` z ) ) )
3635eleq1d 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( n = ( f ` z ) -> ( ( `' f ` n ) e. ( ~P B \ { (/) } ) <-> ( `' f ` ( f ` z ) ) e. ( ~P B \ { (/) } ) ) )
3736rspcev 3070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( f ` z ) e. ran f /\ ( `' f ` ( f ` z ) ) e. ( ~P B \ { (/) } ) ) -> E. n e. ran f ( `' f ` n ) e. ( ~P B \ { (/) } ) )
3821, 34, 37syl2anc 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( 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 \ { (/) } ) )
39 rabn0 3654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } =/= (/) <-> E. n e. ran f ( `' f ` n ) e. ( ~P B \ { (/) } ) )
4038, 39sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 \ { (/) } ) } =/= (/) )
41 onint 6405 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { 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 \ { (/) } ) } )
4216, 40, 41syl2anc 656 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 \ { (/) } ) } )
4342rexlimdvaa 2840 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 \ { (/) } ) } ) )
4413, 43syl5 32 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 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 \ { (/) } ) } ) )
4544expdimp 437 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 \ { (/) } ) } ) )
4645exlimdv 1695 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 \ { (/) } ) } ) )
4712, 46syl5bi 217 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 \ { (/) } ) } ) )
4847expimpd 600 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 \ { (/) } ) } ) )
4911, 48syl5bi 217 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 \ { (/) } ) } ) )
5049impr 616 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 \ { (/) } ) } )
5110, 50sseldd 3354 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
5251expr 612 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) )
5352ralimdva 2792 . . . . . . . . . . . . . . 15 |- ( ( 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 ) )
5453imp 429 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
5554adantrr 711 . . . . . . . . . . . . 13 |- ( ( ( 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 )
56 eqid 2441 . . . . . . . . . . . . . 14 |- ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) = ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
5756fmpt 5861 . . . . . . . . . . . . 13 |- ( 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 )
5855, 57sylib 196 . . . . . . . . . . . 12 |- ( ( ( 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 )
59 neeq1 2614 . . . . . . . . . . . . . . . . . . 19 |- ( ( `' f ` z ) = if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> ( ( `' f ` z ) =/= (/) <-> if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/) ) )
60 neeq1 2614 . . . . . . . . . . . . . . . . . . 19 |- ( 1o = if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) -> ( 1o =/= (/) <-> if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/) ) )
61 1n0 6931 . . . . . . . . . . . . . . . . . . 19 |- 1o =/= (/)
6259, 60, 61elimhyp 3845 . . . . . . . . . . . . . . . . . 18 |- if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/)
63 n0 3643 . . . . . . . . . . . . . . . . . 18 |- ( if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) =/= (/) <-> E. y y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) )
6462, 63mpbi 208 . . . . . . . . . . . . . . . . 17 |- E. y y e. if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o )
65 19.29r 1656 . . . . . . . . . . . . . . . . 17 |- ( ( 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 ) )
6664, 65mpan 665 . . . . . . . . . . . . . . . 16 |- ( 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 ) )
67 eleq1 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 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 \ { (/) } ) } ) )
6850, 67syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( 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 \ { (/) } ) } ) )
6968imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( 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 \ { (/) } ) } )
70 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( n = z -> ( `' f ` n ) = ( `' f ` z ) )
7170eleq1d 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( n = z -> ( ( `' f ` n ) e. ( ~P B \ { (/) } ) <-> ( `' f ` z ) e. ( ~P B \ { (/) } ) ) )
7271elrab 3114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( z e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } <-> ( z e. ran f /\ ( `' f ` z ) e. ( ~P B \ { (/) } ) ) )
7372simprbi 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( z e. { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } -> ( `' f ` z ) e. ( ~P B \ { (/) } ) )
7469, 73syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( 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 \ { (/) } ) )
75 eldifsn 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( `' f ` z ) e. ( ~P B \ { (/) } ) <-> ( ( `' f ` z ) e. ~P B /\ ( `' f ` z ) =/= (/) ) )
7674, 75sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( 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 ) =/= (/) ) )
7776simprd 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 ) =/= (/) )
78 iftrue 3794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( `' f ` z ) =/= (/) -> if ( ( `' f ` z ) =/= (/) , ( `' f ` z ) , 1o ) = ( `' f ` z ) )
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 ) )
8076simpld 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 )
8180elpwid 3867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 )
8279, 81eqsstrd 3387 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( 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 )
8382sseld 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 ) )
8483exp31 601 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 ) ) ) )
8584com23 78 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) ) ) )
8685exp4a 603 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 ) ) ) ) )
8786com25 91 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) ) ) ) )
8887imp31 432 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) ) )
8988ralimdva 2792 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) )
9089imp 429 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) )
9190an32s 797 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 ) )
92 rmoim 3155 . . . . . . . . . . . . . . . . . . 19 |- ( 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 \ { (/) } ) } ) )
9391, 92syl 16 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 \ { (/) } ) } ) )
9493expimpd 600 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 \ { (/) } ) } ) )
9594exlimdv 1695 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 \ { (/) } ) } ) )
9666, 95syl5 32 . . . . . . . . . . . . . . 15 |- ( ( ( 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 \ { (/) } ) } ) )
9796impr 616 . . . . . . . . . . . . . 14 |- ( ( ( 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 \ { (/) } ) } )
98 nfcv 2577 . . . . . . . . . . . . . . . . 17 |- F/_ x w
99 nfmpt1 4378 . . . . . . . . . . . . . . . . 17 |- F/_ x ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
100 nfcv 2577 . . . . . . . . . . . . . . . . 17 |- F/_ x z
10198, 99, 100nfbr 4333 . . . . . . . . . . . . . . . 16 |- F/ x w ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) z
102 nfv 1678 . . . . . . . . . . . . . . . 16 |- F/ w ( x e. A /\ z = |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } )
103 breq1 4292 . . . . . . . . . . . . . . . . 17 |- ( 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 ) )
104 df-br 4290 . . . . . . . . . . . . . . . . . 18 |- ( 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 \ { (/) } ) } ) )
105 df-mpt 4349 . . . . . . . . . . . . . . . . . . 19 |- ( 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 \ { (/) } ) } ) }
106105eleq2i 2505 . . . . . . . . . . . . . . . . . 18 |- ( <. 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 \ { (/) } ) } ) } )
107 opabid 4593 . . . . . . . . . . . . . . . . . 18 |- ( <. 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 \ { (/) } ) } ) )
108104, 106, 1073bitri 271 . . . . . . . . . . . . . . . . 17 |- ( 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 \ { (/) } ) } ) )
109103, 108syl6bb 261 . . . . . . . . . . . . . . . 16 |- ( 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 \ { (/) } ) } ) ) )
110101, 102, 109cbvmo 2302 . . . . . . . . . . . . . . 15 |- ( 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 \ { (/) } ) } ) )
111 df-rmo 2721 . . . . . . . . . . . . . . 15 |- ( 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 \ { (/) } ) } ) )
112110, 111bitr4i 252 . . . . . . . . . . . . . 14 |- ( 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 \ { (/) } ) } )
11397, 112sylibr 212 . . . . . . . . . . . . 13 |- ( ( ( 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 )
114113alrimiv 1690 . . . . . . . . . . . 12 |- ( ( ( 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 )
115 dff12 5602 . . . . . . . . . . . 12 |- ( ( 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 ) )
11658, 114, 115sylanbrc 659 . . . . . . . . . . 11 |- ( ( ( 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 )
117 f1domg 7325 . . . . . . . . . . 11 |- ( om e. _V -> ( ( x e. A |-> |^| { n e. ran f | ( `' f ` n ) e. ( ~P B \ { (/) } ) } ) : A -1-1-> om -> A ~<_ om ) )
1182, 116, 117mpsyl 63 . . . . . . . . . 10 |- ( ( ( 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 )
119118ex 434 . . . . . . . . 9 |- ( ( 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 ) )
120 difeq1 3464 . . . . . . . . . . . . 13 |- ( ( topGen ` b ) = J -> ( ( topGen ` b ) \ { (/) } ) = ( J \ { (/) } ) )
121120eleq2d 2508 . . . . . . . . . . . 12 |- ( ( topGen ` b ) = J -> ( B e. ( ( topGen ` b ) \ { (/) } ) <-> B e. ( J \ { (/) } ) ) )
122121ralbidv 2733 . . . . . . . . . . 11 |- ( ( topGen ` b ) = J -> ( A. x e. A B e. ( ( topGen ` b ) \ { (/) } ) <-> A. x e. A B e. ( J \ { (/) } ) ) )
123122anbi1d 699 . . . . . . . . . 10 |- ( ( 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 ) ) )
124123imbi1d 317 . . . . . . . . 9 |- ( ( 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 ) ) )
125119, 124syl5ibcom 220 . . . . . . . 8 |- ( ( 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 ) ) )
126125ex 434 . . . . . . 7 |- ( 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 ) ) ) )
127126exlimdv 1695 . . . . . 6 |- ( 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 ) ) ) )
1283, 127syl5bi 217 . . . . 5 |- ( 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 ) ) ) )
129128imp3a 431 . . . 4 |- ( 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 ) ) )
130129rexlimiv 2833 . . 3 |- ( 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 ) )
1311, 130sylbi 195 . 2 |- ( J e. 2ndc -> ( ( A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ om ) )
1321313impib 1180 1 |- ( ( J e. 2ndc /\ A. x e. A B e. ( J \ { (/) } ) /\ A. y E* x e. A y e. B ) -> A ~<_ om )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 960   A.wal 1362   = wceq 1364   E.wex 1591   e. wcel 1761   E*wmo 2260   =/= wne 2604   A.wral 2713   E.wrex 2714   E*wrmo 2716   {crab 2717   _Vcvv 2970   \ cdif 3322   C_ wss 3325   (/)c0 3634   ifcif 3788   ~Pcpw 3857   {csn 3874   <.cop 3880   |^|cint 4125   class class class wbr 4289   {copab 4346   e. cmpt 4347   Oncon0 4715   `'ccnv 4835   ran crn 4837   Fn wfn 5410   -->wf 5411   -1-1->wf1 5412   -1-1-onto->wf1o 5414   ` cfv 5415   omcom 6475   1oc1o 6909   ~<_ cdom 7304   topGenctg 14372   TopBasesctb 18402   2ndcc2ndc 18942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-om 6476  df-1o 6916  df-dom 7308  df-topgen 14378  df-2ndc 18944
This theorem is referenced by:  2ndcdisj2  18961
  Copyright terms: Public domain W3C validator