Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  comppfsc Unicode version

Theorem comppfsc 26410
Description: A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypothesis
Ref Expression
comppfsc.1  |-  X  = 
U. J
Assertion
Ref Expression
comppfsc  |-  ( J  e.  Top  ->  ( J  e.  Comp  <->  A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) ) ) )
Distinct variable groups:    c, d, J    X, c, d

Proof of Theorem comppfsc
Dummy variables  a 
b  f  p  q  s  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpwi 3646 . . . 4  |-  ( c  e.  ~P J  -> 
c  C_  J )
2 comppfsc.1 . . . . . . 7  |-  X  = 
U. J
32cmpcov 17132 . . . . . 6  |-  ( ( J  e.  Comp  /\  c  C_  J  /\  X  = 
U. c )  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)
4 elfpw 7173 . . . . . . . 8  |-  ( d  e.  ( ~P c  i^i  Fin )  <->  ( d  C_  c  /\  d  e. 
Fin ) )
5 finptfin 26400 . . . . . . . . . . 11  |-  ( d  e.  Fin  ->  d  e.  PtFin )
65anim1i 551 . . . . . . . . . 10  |-  ( ( d  e.  Fin  /\  ( d  C_  c  /\  X  =  U. d ) )  -> 
( d  e.  PtFin  /\  ( d  C_  c  /\  X  =  U. d ) ) )
76anassrs 629 . . . . . . . . 9  |-  ( ( ( d  e.  Fin  /\  d  C_  c )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
87ancom1s 780 . . . . . . . 8  |-  ( ( ( d  C_  c  /\  d  e.  Fin )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
94, 8sylanb 458 . . . . . . 7  |-  ( ( d  e.  ( ~P c  i^i  Fin )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
109reximi2 2662 . . . . . 6  |-  ( E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) )
113, 10syl 15 . . . . 5  |-  ( ( J  e.  Comp  /\  c  C_  J  /\  X  = 
U. c )  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )
12113exp 1150 . . . 4  |-  ( J  e.  Comp  ->  ( c 
C_  J  ->  ( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) ) ) )
131, 12syl5 28 . . 3  |-  ( J  e.  Comp  ->  ( c  e.  ~P J  -> 
( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) ) ) )
1413ralrimiv 2638 . 2  |-  ( J  e.  Comp  ->  A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) ) )
15 elpwi 3646 . . . . . . 7  |-  ( a  e.  ~P J  -> 
a  C_  J )
16 0elpw 4196 . . . . . . . . . . 11  |-  (/)  e.  ~P a
17 0fin 7103 . . . . . . . . . . 11  |-  (/)  e.  Fin
18 elin 3371 . . . . . . . . . . 11  |-  ( (/)  e.  ( ~P a  i^i 
Fin )  <->  ( (/)  e.  ~P a  /\  (/)  e.  Fin )
)
1916, 17, 18mpbir2an 886 . . . . . . . . . 10  |-  (/)  e.  ( ~P a  i^i  Fin )
20 unieq 3852 . . . . . . . . . . . . 13  |-  ( b  =  (/)  ->  U. b  =  U. (/) )
21 uni0 3870 . . . . . . . . . . . . 13  |-  U. (/)  =  (/)
2220, 21syl6eq 2344 . . . . . . . . . . . 12  |-  ( b  =  (/)  ->  U. b  =  (/) )
2322eqeq2d 2307 . . . . . . . . . . 11  |-  ( b  =  (/)  ->  ( X  =  U. b  <->  X  =  (/) ) )
2423rspcev 2897 . . . . . . . . . 10  |-  ( (
(/)  e.  ( ~P a  i^i  Fin )  /\  X  =  (/) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
)
2519, 24mpan 651 . . . . . . . . 9  |-  ( X  =  (/)  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b )
2625a1i13 26303 . . . . . . . 8  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( X  =  (/)  ->  ( A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) ) )
27 n0 3477 . . . . . . . . 9  |-  ( X  =/=  (/)  <->  E. x  x  e.  X )
28 simp2 956 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  X  =  U. a )
2928eleq2d 2363 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  <->  x  e.  U. a
) )
3029biimpd 198 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  ->  x  e.  U. a ) )
31 eluni2 3847 . . . . . . . . . . . 12  |-  ( x  e.  U. a  <->  E. s  e.  a  x  e.  s )
3230, 31syl6ib 217 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  ->  E. s  e.  a  x  e.  s ) )
33 simpl3 960 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
a  C_  J )
34 simprl 732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  a )
3533, 34sseldd 3194 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
36 elssuni 3871 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  J  ->  s  C_ 
U. J )
3736, 2syl6sseqr 3238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  J  ->  s  C_  X )
3835, 37syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  C_  X )
3938ralrimivw 2640 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  A. p  e.  a 
s  C_  X )
40 iunss 3959 . . . . . . . . . . . . . . . . . . 19  |-  ( U_ p  e.  a  s  C_  X  <->  A. p  e.  a  s  C_  X )
4139, 40sylibr 203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  U_ p  e.  a 
s  C_  X )
42 ssequn1 3358 . . . . . . . . . . . . . . . . . 18  |-  ( U_ p  e.  a  s  C_  X  <->  ( U_ p  e.  a  s  u.  X )  =  X )
4341, 42sylib 188 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( U_ p  e.  a  s  u.  X )  =  X )
44 simpl2 959 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U. a
)
45 uniiun 3971 . . . . . . . . . . . . . . . . . . 19  |-  U. a  =  U_ p  e.  a  p
4644, 45syl6eq 2344 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U_ p  e.  a  p )
4746uneq2d 3342 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( U_ p  e.  a  s  u.  X )  =  ( U_ p  e.  a  s  u.  U_ p  e.  a  p ) )
4843, 47eqtr3d 2330 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  ( U_ p  e.  a  s  u.  U_ p  e.  a  p ) )
49 iunun 3998 . . . . . . . . . . . . . . . . 17  |-  U_ p  e.  a  ( s  u.  p )  =  (
U_ p  e.  a  s  u.  U_ p  e.  a  p )
50 vex 2804 . . . . . . . . . . . . . . . . . . 19  |-  s  e. 
_V
51 vex 2804 . . . . . . . . . . . . . . . . . . 19  |-  p  e. 
_V
5250, 51unex 4534 . . . . . . . . . . . . . . . . . 18  |-  ( s  u.  p )  e. 
_V
5352dfiun3 4949 . . . . . . . . . . . . . . . . 17  |-  U_ p  e.  a  ( s  u.  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5449, 53eqtr3i 2318 . . . . . . . . . . . . . . . 16  |-  ( U_ p  e.  a  s  u.  U_ p  e.  a  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5548, 54syl6eq 2344 . . . . . . . . . . . . . . 15  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U. ran  (
p  e.  a  |->  ( s  u.  p ) ) )
56 simpll1 994 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  J  e.  Top )
5735adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  s  e.  J )
5833sselda 3193 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  p  e.  J )
59 unopn 16665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( J  e.  Top  /\  s  e.  J  /\  p  e.  J )  ->  ( s  u.  p
)  e.  J )
6056, 57, 58, 59syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  (
s  u.  p )  e.  J )
61 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  ( p  e.  a  |->  ( s  u.  p ) )  =  ( p  e.  a  |->  ( s  u.  p ) )
6260, 61fmptd 5700 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( p  e.  a 
|->  ( s  u.  p
) ) : a --> J )
63 frn 5411 . . . . . . . . . . . . . . . . . 18  |-  ( ( p  e.  a  |->  ( s  u.  p ) ) : a --> J  ->  ran  ( p  e.  a  |->  ( s  u.  p ) ) 
C_  J )
6462, 63syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  ran  ( p  e.  a 
|->  ( s  u.  p
) )  C_  J
)
65 elpw2g 4190 . . . . . . . . . . . . . . . . . . 19  |-  ( J  e.  Top  ->  ( ran  ( p  e.  a 
|->  ( s  u.  p
) )  e.  ~P J 
<->  ran  ( p  e.  a  |->  ( s  u.  p ) )  C_  J ) )
66653ad2ant1 976 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( ran  (
p  e.  a  |->  ( s  u.  p ) )  e.  ~P J  <->  ran  ( p  e.  a 
|->  ( s  u.  p
) )  C_  J
) )
6766adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( ran  ( p  e.  a  |->  ( s  u.  p ) )  e.  ~P J  <->  ran  ( p  e.  a  |->  ( s  u.  p ) ) 
C_  J ) )
6864, 67mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  ran  ( p  e.  a 
|->  ( s  u.  p
) )  e.  ~P J )
69 unieq 3852 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  U. c  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) ) )
7069eqeq2d 2307 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( X  = 
U. c  <->  X  =  U. ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
71 sseq2 3213 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( d  C_  c 
<->  d  C_  ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
7271anbi1d 685 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( ( d 
C_  c  /\  X  =  U. d )  <->  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) ) )
7372rexbidv 2577 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d )  <->  E. d  e.  PtFin  ( d  C_  ran  ( p  e.  a 
|->  ( s  u.  p
) )  /\  X  =  U. d ) ) )
7470, 73imbi12d 311 . . . . . . . . . . . . . . . . 17  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  <-> 
( X  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )  ->  E. d  e.  PtFin  ( d  C_  ran  ( p  e.  a 
|->  ( s  u.  p
) )  /\  X  =  U. d ) ) ) )
7574rspcv 2893 . . . . . . . . . . . . . . . 16  |-  ( ran  ( p  e.  a 
|->  ( s  u.  p
) )  e.  ~P J  ->  ( A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  ( X  = 
U. ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  E. d  e.  PtFin  ( d  C_  ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d ) ) ) )
7668, 75syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( A. c  e. 
~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  ( X  = 
U. ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  E. d  e.  PtFin  ( d  C_  ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d ) ) ) )
7755, 76mpid 37 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( A. c  e. 
~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  E. d  e.  PtFin  ( d  C_  ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d ) ) )
78 simprr 733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  s )
79 ssel2 3188 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( a  C_  J  /\  s  e.  a )  ->  s  e.  J )
80793ad2antl3 1119 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  s  e.  a )  ->  s  e.  J )
8180adantrr 697 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
82 elunii 3848 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  s  /\  s  e.  J )  ->  x  e.  U. J
)
8378, 81, 82syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  U. J )
8483, 2syl6eleqr 2387 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  X )
8584adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  x  e.  X )
86 simprr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  X  =  U. d )
8785, 86eleqtrd 2372 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  x  e.  U. d )
88 eqid 2296 . . . . . . . . . . . . . . . . . . . . 21  |-  U. d  =  U. d
8988ptfinfin 26401 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  e.  PtFin  /\  x  e.  U. d )  ->  { z  e.  d  |  x  e.  z }  e.  Fin )
9089expcom 424 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  U. d  -> 
( d  e.  PtFin  ->  { z  e.  d  |  x  e.  z }  e.  Fin )
)
9187, 90syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  (
d  e.  PtFin  ->  { z  e.  d  |  x  e.  z }  e.  Fin ) )
92 simprl 732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) ) )
93 elun1 3355 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  s  ->  x  e.  ( s  u.  p
) )
9493ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  ( s  u.  p ) )
9594ralrimivw 2640 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  A. p  e.  a  x  e.  ( s  u.  p ) )
9652rgenw 2623 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  A. p  e.  a  ( s  u.  p )  e.  _V
97 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  ( s  u.  p )  ->  (
x  e.  z  <->  x  e.  ( s  u.  p
) ) )
9861, 97ralrnmpt 5685 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. p  e.  a  (
s  u.  p )  e.  _V  ->  ( A. z  e.  ran  ( p  e.  a  |->  ( s  u.  p
) ) x  e.  z  <->  A. p  e.  a  x  e.  ( s  u.  p ) ) )
9996, 98ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. z  e.  ran  ( p  e.  a  |->  ( s  u.  p ) ) x  e.  z  <->  A. p  e.  a  x  e.  ( s  u.  p
) )
10095, 99sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  A. z  e.  ran  ( p  e.  a  |->  ( s  u.  p
) ) x  e.  z )
101100adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  A. z  e.  ran  ( p  e.  a  |->  ( s  u.  p ) ) x  e.  z )
102 ssralv 3250 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d 
C_  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( A. z  e.  ran  ( p  e.  a  |->  ( s  u.  p ) ) x  e.  z  ->  A. z  e.  d  x  e.  z ) )
10392, 101, 102sylc 56 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  A. z  e.  d  x  e.  z )
104 rabid2 2730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  =  { z  e.  d  |  x  e.  z }  <->  A. z  e.  d  x  e.  z )
105103, 104sylibr 203 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  d  =  { z  e.  d  |  x  e.  z } )
106105eleq1d 2362 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  (
d  e.  Fin  <->  { z  e.  d  |  x  e.  z }  e.  Fin ) )
107106biimprd 214 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  ( { z  e.  d  |  x  e.  z }  e.  Fin  ->  d  e.  Fin ) )
10861rnmpt 4941 . . . . . . . . . . . . . . . . . . . . . 22  |-  ran  (
p  e.  a  |->  ( s  u.  p ) )  =  { q  |  E. p  e.  a  q  =  ( s  u.  p ) }
10992, 108syl6sseq 3237 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  d  C_ 
{ q  |  E. p  e.  a  q  =  ( s  u.  p ) } )
110 ssabral 3257 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d 
C_  { q  |  E. p  e.  a  q  =  ( s  u.  p ) }  <->  A. q  e.  d  E. p  e.  a 
q  =  ( s  u.  p ) )
111109, 110sylib 188 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  A. q  e.  d  E. p  e.  a  q  =  ( s  u.  p
) )
112 uneq2 3336 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  =  ( f `  q )  ->  (
s  u.  p )  =  ( s  u.  ( f `  q
) ) )
113112eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  =  ( f `  q )  ->  (
q  =  ( s  u.  p )  <->  q  =  ( s  u.  (
f `  q )
) ) )
114113ac6sfi 7117 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( d  e.  Fin  /\  A. q  e.  d  E. p  e.  a  q  =  ( s  u.  p ) )  ->  E. f ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `  q
) ) ) )
115114expcom 424 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. q  e.  d  E. p  e.  a  q  =  ( s  u.  p )  ->  (
d  e.  Fin  ->  E. f ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `  q
) ) ) ) )
116111, 115syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  (
d  e.  Fin  ->  E. f ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `  q
) ) ) ) )
117 frn 5411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : d --> a  ->  ran  f  C_  a )
118117adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `
 q ) ) )  ->  ran  f  C_  a )
119118ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  ran  f  C_  a )
12034ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  s  e.  a )
121120snssd 3776 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  { s } 
C_  a )
122119, 121unssd 3364 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  ( ran  f  u.  { s } ) 
C_  a )
123 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  d  e.  Fin )
124 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  f : d --> a )
125 ffn 5405 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : d --> a  -> 
f  Fn  d )
126124, 125syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  f  Fn  d
)
127 dffn4 5473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  Fn  d  <->  f :
d -onto-> ran  f )
128126, 127sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  f : d
-onto->
ran  f )
129 fofi 7158 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  Fin  /\  f : d -onto-> ran  f
)  ->  ran  f  e. 
Fin )
130123, 128, 129syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  ran  f  e.  Fin )
131 snfi 6957 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { s }  e.  Fin
132 unfi 7140 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ran  f  e.  Fin  /\ 
{ s }  e.  Fin )  ->  ( ran  f  u.  { s } )  e.  Fin )
133130, 131, 132sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  ( ran  f  u.  { s } )  e.  Fin )
134 elfpw 7173 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  f  u.  {
s } )  e.  ( ~P a  i^i 
Fin )  <->  ( ( ran  f  u.  { s } )  C_  a  /\  ( ran  f  u. 
{ s } )  e.  Fin ) )
135122, 133, 134sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  ( ran  f  u.  { s } )  e.  ( ~P a  i^i  Fin ) )
136 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  X  =  U. d )
137 uniiun 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  U. d  =  U_ q  e.  d  q
138 simprrr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  A. q  e.  d  q  =  ( s  u.  ( f `  q ) ) )
139 iuneq2 3937 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A. q  e.  d  q  =  ( s  u.  ( f `  q
) )  ->  U_ q  e.  d  q  =  U_ q  e.  d  ( s  u.  ( f `
 q ) ) )
140138, 139syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  U_ q  e.  d  q  =  U_ q  e.  d  ( s  u.  ( f `  q
) ) )
141137, 140syl5eq 2340 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  U. d  =  U_ q  e.  d  (
s  u.  ( f `
 q ) ) )
142136, 141eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  X  =  U_ q  e.  d  (
s  u.  ( f `
 q ) ) )
143 ssun2 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  { s }  C_  ( ran  f  u.  { s } )
14450snid 3680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  s  e. 
{ s }
145143, 144sselii 3190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  s  e.  ( ran  f  u. 
{ s } )
146 elssuni 3871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  ( ran  f  u.  { s } )  ->  s  C_  U. ( ran  f  u.  { s } ) )
147145, 146ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  s  C_  U. ( ran  f  u. 
{ s } )
148 fvssunirn 5567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f `
 q )  C_  U.
ran  f
149 ssun1 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ran  f  C_  ( ran  f  u. 
{ s } )
150 uniss 3864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ran  f  C_  ( ran  f  u.  { s } )  ->  U. ran  f  C_  U. ( ran  f  u.  { s } ) )
151149, 150ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  U. ran  f  C_  U. ( ran  f  u.  { s } )
152148, 151sstri 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f `
 q )  C_  U. ( ran  f  u. 
{ s } )
153147, 152unssi 3363 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  u.  ( f `  q ) )  C_  U. ( ran  f  u. 
{ s } )
154153rgenw 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  A. q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
155 iunss 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( U_ q  e.  d  (
s  u.  ( f `
 q ) ) 
C_  U. ( ran  f  u.  { s } )  <->  A. q  e.  d 
( s  u.  (
f `  q )
)  C_  U. ( ran  f  u.  { s } ) )
156154, 155mpbir 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U_ q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
157156a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  U_ q  e.  d  ( s  u.  (
f `  q )
)  C_  U. ( ran  f  u.  { s } ) )
158142, 157eqsstrd 3225 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  X  C_  U. ( ran  f  u.  { s } ) )
15933ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  a  C_  J
)
160119, 159sstrd 3202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  ran  f  C_  J )
16135ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  s  e.  J
)
162161snssd 3776 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  { s } 
C_  J )
163160, 162unssd 3364 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  ( ran  f  u.  { s } ) 
C_  J )
164 uniss 3864 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ran  f  u.  {
s } )  C_  J  ->  U. ( ran  f  u.  { s } ) 
C_  U. J )
165164, 2syl6sseqr 3238 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ran  f  u.  {
s } )  C_  J  ->  U. ( ran  f  u.  { s } ) 
C_  X )
166163, 165syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  U. ( ran  f  u.  { s } ) 
C_  X )
167158, 166eqssd 3209 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  X  =  U. ( ran  f  u.  {
s } ) )
168 unieq 3852 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( b  =  ( ran  f  u.  { s } )  ->  U. b  =  U. ( ran  f  u.  {
s } ) )
169168eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  ( ran  f  u.  { s } )  ->  ( X  = 
U. b  <->  X  =  U. ( ran  f  u. 
{ s } ) ) )
170169rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ran  f  u. 
{ s } )  e.  ( ~P a  i^i  Fin )  /\  X  =  U. ( ran  f  u.  { s } ) )  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b )
171135, 167, 170syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  (
d  e.  Fin  /\  ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) ) ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b )
172171expr 598 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  d  e.  Fin )  ->  (
( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) )  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b ) )
173172exlimdv 1626 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  /\  d  e.  Fin )  ->  ( E. f ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `  q
) ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) )
174173ex 423 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  (
d  e.  Fin  ->  ( E. f ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `  q
) ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
175116, 174mpdd 36 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  (
d  e.  Fin  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) )
17691, 107, 1753syld 51 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  ( d  C_ 
ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d
) )  ->  (
d  e.  PtFin  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b ) )
177176ex 423 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( ( d  C_  ran  ( p  e.  a 
|->  ( s  u.  p
) )  /\  X  =  U. d )  -> 
( d  e.  PtFin  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
178177com23 72 . . . . . . . . . . . . . . 15  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( d  e.  PtFin  -> 
( ( d  C_  ran  ( p  e.  a 
|->  ( s  u.  p
) )  /\  X  =  U. d )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
179178rexlimdv 2679 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( E. d  e. 
PtFin  ( d  C_  ran  ( p  e.  a  |->  ( s  u.  p
) )  /\  X  =  U. d )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) )
18077, 179syld 40 . . . . . . . . . . . . 13  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
( A. c  e. 
~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) )
181180expr 598 . . . . . . . . . . . 12  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  s  e.  a )  ->  ( x  e.  s  ->  ( A. c  e.  ~P  J
( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) )  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b ) ) )
182181rexlimdva 2680 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( E. s  e.  a  x  e.  s  ->  ( A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) ) )
18332, 182syld 40 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  ->  ( A. c  e.  ~P  J
( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) )  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b ) ) )
184183exlimdv 1626 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( E. x  x  e.  X  ->  ( A. c  e.  ~P  J ( X  = 
U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
18527, 184syl5bi 208 . . . . . . . 8  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( X  =/=  (/)  ->  ( A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) ) )
18626, 185pm2.61dne 2536 . . . . . . 7  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) )
18715, 186syl3an3 1217 . . . . . 6  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  e.  ~P J )  ->  ( A. c  e.  ~P  J ( X  = 
U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) )
1881873exp 1150 . . . . 5  |-  ( J  e.  Top  ->  ( X  =  U. a  ->  ( a  e.  ~P J  ->  ( A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) ) ) )
189188com24 81 . . . 4  |-  ( J  e.  Top  ->  ( A. c  e.  ~P  J ( X  = 
U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d ) )  -> 
( a  e.  ~P J  ->  ( X  = 
U. a  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b ) ) ) )
190189ralrimdv 2645 . . 3  |-  ( J  e.  Top  ->  ( A. c  e.  ~P  J ( X  = 
U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d ) )  ->  A. a  e.  ~P  J ( X  = 
U. a  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b ) ) )
1912iscmp 17131 . . . 4  |-  ( J  e.  Comp  <->  ( J  e. 
Top  /\  A. a  e.  ~P  J ( X  =  U. a  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
192191baibr 872 . . 3  |-  ( J  e.  Top  ->  ( A. a  e.  ~P  J ( X  = 
U. a  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b )  <->  J  e.  Comp ) )
193190, 192sylibd 205 . 2  |-  ( J  e.  Top  ->  ( A. c  e.  ~P  J ( X  = 
U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d ) )  ->  J  e.  Comp ) )
19414, 193impbid2 195 1  |-  ( J  e.  Top  ->  ( J  e.  Comp  <->  A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934   E.wex 1531    = wceq 1632    e. wcel 1696   {cab 2282    =/= wne 2459   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801    u. cun 3163    i^i cin 3164    C_ wss 3165   (/)c0 3468   ~Pcpw 3638   {csn 3653   U.cuni 3843   U_ciun 3921    e. cmpt 4093   ran crn 4706    Fn wfn 5266   -->wf 5267   -onto->wfo 5269   ` cfv 5271   Fincfn 6879   Topctop 16647   Compccmp 17129   PtFincptfin 26364
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-recs 6404  df-rdg 6439  df-1o 6495  df-oadd 6499  df-er 6676  df-en 6880  df-dom 6881  df-fin 6883  df-top 16652  df-cmp 17130  df-ptfin 26368
  Copyright terms: Public domain W3C validator