MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fclsfnflim Structured version   Unicode version

Theorem fclsfnflim 20820
Description: A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
Assertion
Ref Expression
fclsfnflim  |-  ( F  e.  ( Fil `  X
)  ->  ( A  e.  ( J  fClus  F )  <->  E. g  e.  ( Fil `  X ) ( F  C_  g  /\  A  e.  ( J  fLim  g ) ) ) )
Distinct variable groups:    A, g    g, F    g, J    g, X

Proof of Theorem fclsfnflim
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 filsspw 20644 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  F  C_  ~P X )
21adantr 463 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  F  C_  ~P X )
3 fclstop 20804 . . . . . . . . . 10  |-  ( A  e.  ( J  fClus  F )  ->  J  e.  Top )
43adantl 464 . . . . . . . . 9  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  J  e.  Top )
5 eqid 2402 . . . . . . . . . 10  |-  U. J  =  U. J
65neisspw 19901 . . . . . . . . 9  |-  ( J  e.  Top  ->  (
( nei `  J
) `  { A } )  C_  ~P U. J )
74, 6syl 17 . . . . . . . 8  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( ( nei `  J ) `  { A } )  C_  ~P U. J )
8 filunibas 20674 . . . . . . . . . 10  |-  ( F  e.  ( Fil `  X
)  ->  U. F  =  X )
95fclsfil 20803 . . . . . . . . . . 11  |-  ( A  e.  ( J  fClus  F )  ->  F  e.  ( Fil `  U. J
) )
10 filunibas 20674 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  U. J )  ->  U. F  =  U. J )
119, 10syl 17 . . . . . . . . . 10  |-  ( A  e.  ( J  fClus  F )  ->  U. F  = 
U. J )
128, 11sylan9req 2464 . . . . . . . . 9  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  X  =  U. J )
1312pweqd 3960 . . . . . . . 8  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ~P X  =  ~P U. J )
147, 13sseqtr4d 3479 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( ( nei `  J ) `  { A } )  C_  ~P X )
152, 14unssd 3619 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( F  u.  ( ( nei `  J
) `  { A } ) )  C_  ~P X )
16 ssun1 3606 . . . . . . . 8  |-  F  C_  ( F  u.  (
( nei `  J
) `  { A } ) )
17 filn0 20655 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  F  =/=  (/) )
18 ssn0 3772 . . . . . . . 8  |-  ( ( F  C_  ( F  u.  ( ( nei `  J
) `  { A } ) )  /\  F  =/=  (/) )  ->  ( F  u.  ( ( nei `  J ) `  { A } ) )  =/=  (/) )
1916, 17, 18sylancr 661 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  ( F  u.  ( ( nei `  J
) `  { A } ) )  =/=  (/) )
2019adantr 463 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( F  u.  ( ( nei `  J
) `  { A } ) )  =/=  (/) )
21 incom 3632 . . . . . . . . . . . 12  |-  ( y  i^i  x )  =  ( x  i^i  y
)
22 fclsneii 20810 . . . . . . . . . . . 12  |-  ( ( A  e.  ( J 
fClus  F )  /\  y  e.  ( ( nei `  J
) `  { A } )  /\  x  e.  F )  ->  (
y  i^i  x )  =/=  (/) )
2321, 22syl5eqner 2704 . . . . . . . . . . 11  |-  ( ( A  e.  ( J 
fClus  F )  /\  y  e.  ( ( nei `  J
) `  { A } )  /\  x  e.  F )  ->  (
x  i^i  y )  =/=  (/) )
24233com23 1203 . . . . . . . . . 10  |-  ( ( A  e.  ( J 
fClus  F )  /\  x  e.  F  /\  y  e.  ( ( nei `  J
) `  { A } ) )  -> 
( x  i^i  y
)  =/=  (/) )
25243expb 1198 . . . . . . . . 9  |-  ( ( A  e.  ( J 
fClus  F )  /\  (
x  e.  F  /\  y  e.  ( ( nei `  J ) `  { A } ) ) )  ->  ( x  i^i  y )  =/=  (/) )
2625adantll 712 . . . . . . . 8  |-  ( ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F )
)  /\  ( x  e.  F  /\  y  e.  ( ( nei `  J
) `  { A } ) ) )  ->  ( x  i^i  y )  =/=  (/) )
2726ralrimivva 2825 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  A. x  e.  F  A. y  e.  ( ( nei `  J
) `  { A } ) ( x  i^i  y )  =/=  (/) )
28 filfbas 20641 . . . . . . . . 9  |-  ( F  e.  ( Fil `  X
)  ->  F  e.  ( fBas `  X )
)
2928adantr 463 . . . . . . . 8  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  F  e.  ( fBas `  X )
)
30 istopon 19718 . . . . . . . . . . 11  |-  ( J  e.  (TopOn `  X
)  <->  ( J  e. 
Top  /\  X  =  U. J ) )
314, 12, 30sylanbrc 662 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  J  e.  (TopOn `  X ) )
325fclselbas 20809 . . . . . . . . . . . . 13  |-  ( A  e.  ( J  fClus  F )  ->  A  e.  U. J )
3332adantl 464 . . . . . . . . . . . 12  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  A  e.  U. J )
3433, 12eleqtrrd 2493 . . . . . . . . . . 11  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  A  e.  X )
3534snssd 4117 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  { A }  C_  X )
36 snnzg 4089 . . . . . . . . . . 11  |-  ( A  e.  ( J  fClus  F )  ->  { A }  =/=  (/) )
3736adantl 464 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  { A }  =/=  (/) )
38 neifil 20673 . . . . . . . . . 10  |-  ( ( J  e.  (TopOn `  X )  /\  { A }  C_  X  /\  { A }  =/=  (/) )  -> 
( ( nei `  J
) `  { A } )  e.  ( Fil `  X ) )
3931, 35, 37, 38syl3anc 1230 . . . . . . . . 9  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( ( nei `  J ) `  { A } )  e.  ( Fil `  X
) )
40 filfbas 20641 . . . . . . . . 9  |-  ( ( ( nei `  J
) `  { A } )  e.  ( Fil `  X )  ->  ( ( nei `  J ) `  { A } )  e.  (
fBas `  X )
)
4139, 40syl 17 . . . . . . . 8  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( ( nei `  J ) `  { A } )  e.  ( fBas `  X
) )
42 fbunfip 20662 . . . . . . . 8  |-  ( ( F  e.  ( fBas `  X )  /\  (
( nei `  J
) `  { A } )  e.  (
fBas `  X )
)  ->  ( -.  (/) 
e.  ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) )  <->  A. x  e.  F  A. y  e.  (
( nei `  J
) `  { A } ) ( x  i^i  y )  =/=  (/) ) )
4329, 41, 42syl2anc 659 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( -.  (/) 
e.  ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) )  <->  A. x  e.  F  A. y  e.  (
( nei `  J
) `  { A } ) ( x  i^i  y )  =/=  (/) ) )
4427, 43mpbird 232 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  -.  (/)  e.  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )
45 filtop 20648 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
46 fsubbas 20660 . . . . . . . 8  |-  ( X  e.  F  ->  (
( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) )  e.  ( fBas `  X )  <->  ( ( F  u.  ( ( nei `  J ) `  { A } ) ) 
C_  ~P X  /\  ( F  u.  ( ( nei `  J ) `  { A } ) )  =/=  (/)  /\  -.  (/)  e.  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) ) )
4745, 46syl 17 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  ( ( fi `  ( F  u.  ( ( nei `  J
) `  { A } ) ) )  e.  ( fBas `  X
)  <->  ( ( F  u.  ( ( nei `  J ) `  { A } ) )  C_  ~P X  /\  ( F  u.  ( ( nei `  J ) `  { A } ) )  =/=  (/)  /\  -.  (/)  e.  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) ) )
4847adantr 463 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( ( fi `  ( F  u.  ( ( nei `  J
) `  { A } ) ) )  e.  ( fBas `  X
)  <->  ( ( F  u.  ( ( nei `  J ) `  { A } ) )  C_  ~P X  /\  ( F  u.  ( ( nei `  J ) `  { A } ) )  =/=  (/)  /\  -.  (/)  e.  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) ) )
4915, 20, 44, 48mpbir3and 1180 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) )  e.  ( fBas `  X
) )
50 fgcl 20671 . . . . 5  |-  ( ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) )  e.  ( fBas `  X
)  ->  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )  e.  ( Fil `  X ) )
5149, 50syl 17 . . . 4  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )  e.  ( Fil `  X ) )
52 fvex 5859 . . . . . . . . 9  |-  ( ( nei `  J ) `
 { A }
)  e.  _V
53 unexg 6583 . . . . . . . . 9  |-  ( ( F  e.  ( Fil `  X )  /\  (
( nei `  J
) `  { A } )  e.  _V )  ->  ( F  u.  ( ( nei `  J
) `  { A } ) )  e. 
_V )
5452, 53mpan2 669 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  ( F  u.  ( ( nei `  J
) `  { A } ) )  e. 
_V )
55 ssfii 7913 . . . . . . . 8  |-  ( ( F  u.  ( ( nei `  J ) `
 { A }
) )  e.  _V  ->  ( F  u.  (
( nei `  J
) `  { A } ) )  C_  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )
5654, 55syl 17 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  ( F  u.  ( ( nei `  J
) `  { A } ) )  C_  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )
5756adantr 463 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( F  u.  ( ( nei `  J
) `  { A } ) )  C_  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )
5857unssad 3620 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  F  C_  ( fi `  ( F  u.  ( ( nei `  J
) `  { A } ) ) ) )
59 ssfg 20665 . . . . . 6  |-  ( ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) )  e.  ( fBas `  X
)  ->  ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) 
C_  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) )
6049, 59syl 17 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) 
C_  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) )
6158, 60sstrd 3452 . . . 4  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  F  C_  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) ) )
6257unssbd 3621 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( ( nei `  J ) `  { A } )  C_  ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )
6362, 60sstrd 3452 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( ( nei `  J ) `  { A } )  C_  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) ) )
64 elflim 20764 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) )  e.  ( Fil `  X ) )  -> 
( A  e.  ( J  fLim  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) )  <->  ( A  e.  X  /\  (
( nei `  J
) `  { A } )  C_  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) ) ) ) )
6531, 51, 64syl2anc 659 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  ( A  e.  ( J  fLim  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) ) )  <->  ( A  e.  X  /\  (
( nei `  J
) `  { A } )  C_  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) ) ) ) )
6634, 63, 65mpbir2and 923 . . . 4  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  A  e.  ( J  fLim  ( X
filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) ) )
67 sseq2 3464 . . . . . 6  |-  ( g  =  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )  ->  ( F  C_  g  <->  F  C_  ( X
filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) ) )
68 oveq2 6286 . . . . . . 7  |-  ( g  =  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )  ->  ( J  fLim  g )  =  ( J  fLim  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) ) )
6968eleq2d 2472 . . . . . 6  |-  ( g  =  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )  ->  ( A  e.  ( J  fLim  g
)  <->  A  e.  ( J  fLim  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) ) ) ) )
7067, 69anbi12d 709 . . . . 5  |-  ( g  =  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )  ->  ( ( F  C_  g  /\  A  e.  ( J  fLim  g
) )  <->  ( F  C_  ( X filGen ( fi
`  ( F  u.  ( ( nei `  J
) `  { A } ) ) ) )  /\  A  e.  ( J  fLim  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) ) ) ) ) )
7170rspcev 3160 . . . 4  |-  ( ( ( X filGen ( fi
`  ( F  u.  ( ( nei `  J
) `  { A } ) ) ) )  e.  ( Fil `  X )  /\  ( F  C_  ( X filGen ( fi `  ( F  u.  ( ( nei `  J ) `  { A } ) ) ) )  /\  A  e.  ( J  fLim  ( X filGen ( fi `  ( F  u.  (
( nei `  J
) `  { A } ) ) ) ) ) ) )  ->  E. g  e.  ( Fil `  X ) ( F  C_  g  /\  A  e.  ( J  fLim  g ) ) )
7251, 61, 66, 71syl12anc 1228 . . 3  |-  ( ( F  e.  ( Fil `  X )  /\  A  e.  ( J  fClus  F ) )  ->  E. g  e.  ( Fil `  X
) ( F  C_  g  /\  A  e.  ( J  fLim  g )
) )
7372ex 432 . 2  |-  ( F  e.  ( Fil `  X
)  ->  ( A  e.  ( J  fClus  F )  ->  E. g  e.  ( Fil `  X ) ( F  C_  g  /\  A  e.  ( J  fLim  g ) ) ) )
74 simprl 756 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  g  e.  ( Fil `  X ) )
75 simprrr 767 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  A  e.  ( J  fLim  g )
)
76 flimtopon 20763 . . . . . . 7  |-  ( A  e.  ( J  fLim  g )  ->  ( J  e.  (TopOn `  X )  <->  g  e.  ( Fil `  X
) ) )
7775, 76syl 17 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  ( J  e.  (TopOn `  X )  <->  g  e.  ( Fil `  X
) ) )
7874, 77mpbird 232 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  J  e.  (TopOn `  X ) )
79 simpl 455 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  F  e.  ( Fil `  X ) )
80 simprrl 766 . . . . 5  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  F  C_  g
)
81 fclsss2 20816 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  F  e.  ( Fil `  X
)  /\  F  C_  g
)  ->  ( J  fClus  g )  C_  ( J  fClus  F ) )
8278, 79, 80, 81syl3anc 1230 . . . 4  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  ( J  fClus  g )  C_  ( J  fClus  F ) )
83 flimfcls 20819 . . . . 5  |-  ( J 
fLim  g )  C_  ( J  fClus  g )
8483, 75sseldi 3440 . . . 4  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  A  e.  ( J  fClus  g )
)
8582, 84sseldd 3443 . . 3  |-  ( ( F  e.  ( Fil `  X )  /\  (
g  e.  ( Fil `  X )  /\  ( F  C_  g  /\  A  e.  ( J  fLim  g
) ) ) )  ->  A  e.  ( J  fClus  F )
)
8685rexlimdvaa 2897 . 2  |-  ( F  e.  ( Fil `  X
)  ->  ( E. g  e.  ( Fil `  X ) ( F 
C_  g  /\  A  e.  ( J  fLim  g
) )  ->  A  e.  ( J  fClus  F ) ) )
8773, 86impbid 190 1  |-  ( F  e.  ( Fil `  X
)  ->  ( A  e.  ( J  fClus  F )  <->  E. g  e.  ( Fil `  X ) ( F  C_  g  /\  A  e.  ( J  fLim  g ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367    /\ w3a 974    = wceq 1405    e. wcel 1842    =/= wne 2598   A.wral 2754   E.wrex 2755   _Vcvv 3059    u. cun 3412    i^i cin 3413    C_ wss 3414   (/)c0 3738   ~Pcpw 3955   {csn 3972   U.cuni 4191   ` cfv 5569  (class class class)co 6278   ficfi 7904   fBascfbas 18726   filGencfg 18727   Topctop 19686  TopOnctopon 19687   neicnei 19891   Filcfil 20638    fLim cflim 20727    fClus cfcls 20729
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-iin 4274  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-oadd 7171  df-er 7348  df-en 7555  df-fin 7558  df-fi 7905  df-fbas 18736  df-fg 18737  df-top 19691  df-topon 19694  df-cld 19812  df-ntr 19813  df-cls 19814  df-nei 19892  df-fil 20639  df-flim 20732  df-fcls 20734
This theorem is referenced by:  uffclsflim  20824  cnpfcfi  20833
  Copyright terms: Public domain W3C validator