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

Theorem comppfsc 28726
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 3976 . . . 4  |-  ( c  e.  ~P J  -> 
c  C_  J )
2 comppfsc.1 . . . . . . 7  |-  X  = 
U. J
32cmpcov 19123 . . . . . 6  |-  ( ( J  e.  Comp  /\  c  C_  J  /\  X  = 
U. c )  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)
4 elfpw 7723 . . . . . . . 8  |-  ( d  e.  ( ~P c  i^i  Fin )  <->  ( d  C_  c  /\  d  e. 
Fin ) )
5 finptfin 28716 . . . . . . . . . . 11  |-  ( d  e.  Fin  ->  d  e.  PtFin )
65anim1i 568 . . . . . . . . . 10  |-  ( ( d  e.  Fin  /\  ( d  C_  c  /\  X  =  U. d ) )  -> 
( d  e.  PtFin  /\  ( d  C_  c  /\  X  =  U. d ) ) )
76anassrs 648 . . . . . . . . 9  |-  ( ( ( d  e.  Fin  /\  d  C_  c )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
87ancom1s 803 . . . . . . . 8  |-  ( ( ( d  C_  c  /\  d  e.  Fin )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
94, 8sylanb 472 . . . . . . 7  |-  ( ( d  e.  ( ~P c  i^i  Fin )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
109reximi2 2926 . . . . . 6  |-  ( E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) )
113, 10syl 16 . . . . 5  |-  ( ( J  e.  Comp  /\  c  C_  J  /\  X  = 
U. c )  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) )
12113exp 1187 . . . 4  |-  ( J  e.  Comp  ->  ( c 
C_  J  ->  ( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) ) ) )
131, 12syl5 32 . . 3  |-  ( J  e.  Comp  ->  ( c  e.  ~P J  -> 
( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) ) ) )
1413ralrimiv 2827 . 2  |-  ( J  e.  Comp  ->  A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) ) )
15 elpwi 3976 . . . . . . 7  |-  ( a  e.  ~P J  -> 
a  C_  J )
16 0elpw 4568 . . . . . . . . . . 11  |-  (/)  e.  ~P a
17 0fin 7650 . . . . . . . . . . 11  |-  (/)  e.  Fin
18 elin 3646 . . . . . . . . . . 11  |-  ( (/)  e.  ( ~P a  i^i 
Fin )  <->  ( (/)  e.  ~P a  /\  (/)  e.  Fin )
)
1916, 17, 18mpbir2an 911 . . . . . . . . . 10  |-  (/)  e.  ( ~P a  i^i  Fin )
20 unieq 4206 . . . . . . . . . . . . 13  |-  ( b  =  (/)  ->  U. b  =  U. (/) )
21 uni0 4225 . . . . . . . . . . . . 13  |-  U. (/)  =  (/)
2220, 21syl6eq 2511 . . . . . . . . . . . 12  |-  ( b  =  (/)  ->  U. b  =  (/) )
2322eqeq2d 2468 . . . . . . . . . . 11  |-  ( b  =  (/)  ->  ( X  =  U. b  <->  X  =  (/) ) )
2423rspcev 3177 . . . . . . . . . 10  |-  ( (
(/)  e.  ( ~P a  i^i  Fin )  /\  X  =  (/) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
)
2519, 24mpan 670 . . . . . . . . 9  |-  ( X  =  (/)  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b )
2625a1i13 28637 . . . . . . . 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 3753 . . . . . . . . 9  |-  ( X  =/=  (/)  <->  E. x  x  e.  X )
28 simp2 989 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  X  =  U. a )
2928eleq2d 2524 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  <->  x  e.  U. a
) )
3029biimpd 207 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  ->  x  e.  U. a ) )
31 eluni2 4202 . . . . . . . . . . . 12  |-  ( x  e.  U. a  <->  E. s  e.  a  x  e.  s )
3230, 31syl6ib 226 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  ->  E. s  e.  a  x  e.  s ) )
33 simpl3 993 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
a  C_  J )
34 simprl 755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  a )
3533, 34sseldd 3464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
36 elssuni 4228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  J  ->  s  C_ 
U. J )
3736, 2syl6sseqr 3510 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  J  ->  s  C_  X )
3835, 37syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  C_  X )
3938ralrimivw 2830 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  A. p  e.  a 
s  C_  X )
40 iunss 4318 . . . . . . . . . . . . . . . . . 18  |-  ( U_ p  e.  a  s  C_  X  <->  A. p  e.  a  s  C_  X )
4139, 40sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  U_ p  e.  a 
s  C_  X )
42 ssequn1 3633 . . . . . . . . . . . . . . . . 17  |-  ( U_ p  e.  a  s  C_  X  <->  ( U_ p  e.  a  s  u.  X )  =  X )
4341, 42sylib 196 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 992 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U. a
)
45 uniiun 4330 . . . . . . . . . . . . . . . . . 18  |-  U. a  =  U_ p  e.  a  p
4644, 45syl6eq 2511 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U_ p  e.  a  p )
4746uneq2d 3617 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 2497 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 4358 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  (
U_ p  e.  a  s  u.  U_ p  e.  a  p )
50 vex 3079 . . . . . . . . . . . . . . . . . 18  |-  s  e. 
_V
51 vex 3079 . . . . . . . . . . . . . . . . . 18  |-  p  e. 
_V
5250, 51unex 6487 . . . . . . . . . . . . . . . . 17  |-  ( s  u.  p )  e. 
_V
5352dfiun3 5201 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5449, 53eqtr3i 2485 . . . . . . . . . . . . . . 15  |-  ( U_ p  e.  a  s  u.  U_ p  e.  a  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5548, 54syl6eq 2511 . . . . . . . . . . . . . 14  |-  ( ( ( 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 1027 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  J  e.  Top )
5735adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  s  e.  J )
5833sselda 3463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  p  e.  J )
59 unopn 18647 . . . . . . . . . . . . . . . . . . 19  |-  ( ( J  e.  Top  /\  s  e.  J  /\  p  e.  J )  ->  ( s  u.  p
)  e.  J )
6056, 57, 58, 59syl3anc 1219 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 2454 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  a  |->  ( s  u.  p ) )  =  ( p  e.  a  |->  ( s  u.  p ) )
6260, 61fmptd 5975 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 5672 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  a  |->  ( s  u.  p ) ) : a --> J  ->  ran  ( p  e.  a  |->  ( s  u.  p ) ) 
C_  J )
6462, 63syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 4562 . . . . . . . . . . . . . . . . . 18  |-  ( J  e.  Top  ->  ( ran  ( p  e.  a 
|->  ( s  u.  p
) )  e.  ~P J 
<->  ran  ( p  e.  a  |->  ( s  u.  p ) )  C_  J ) )
66653ad2ant1 1009 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 465 . . . . . . . . . . . . . . . 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  <->  ran  ( p  e.  a  |->  ( s  u.  p ) ) 
C_  J ) )
6864, 67mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 4206 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  U. c  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) ) )
7069eqeq2d 2468 . . . . . . . . . . . . . . . . 17  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( X  = 
U. c  <->  X  =  U. ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
71 sseq2 3485 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( d  C_  c 
<->  d  C_  ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
7271anbi1d 704 . . . . . . . . . . . . . . . . . 18  |-  ( 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 2864 . . . . . . . . . . . . . . . . 17  |-  ( 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 320 . . . . . . . . . . . . . . . 16  |-  ( 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 3173 . . . . . . . . . . . . . . 15  |-  ( 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 16 . . . . . . . . . . . . . 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 ) )  ->  ( 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 41 . . . . . . . . . . . . 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. d  e.  PtFin  ( d  C_  ran  ( p  e.  a  |->  ( s  u.  p ) )  /\  X  =  U. d ) ) )
78 simprr 756 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  s )
79 ssel2 3458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  C_  J  /\  s  e.  a )  ->  s  e.  J )
80793ad2antl3 1152 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  s  e.  a )  ->  s  e.  J )
8180adantrr 716 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
82 elunii 4203 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  s  /\  s  e.  J )  ->  x  e.  U. J
)
8378, 81, 82syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  U. J )
8483, 2syl6eleqr 2553 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  X )
8584adantr 465 . . . . . . . . . . . . . . . . . . 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.  X )
86 simprr 756 . . . . . . . . . . . . . . . . . . 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  =  U. d )
8785, 86eleqtrd 2544 . . . . . . . . . . . . . . . . . 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
) )  ->  x  e.  U. d )
88 eqid 2454 . . . . . . . . . . . . . . . . . . . 20  |-  U. d  =  U. d
8988ptfinfin 28717 . . . . . . . . . . . . . . . . . . 19  |-  ( ( d  e.  PtFin  /\  x  e.  U. d )  ->  { z  e.  d  |  x  e.  z }  e.  Fin )
9089expcom 435 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  U. d  -> 
( d  e.  PtFin  ->  { z  e.  d  |  x  e.  z }  e.  Fin )
)
9187, 90syl 16 . . . . . . . . . . . . . . . . 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  ->  { z  e.  d  |  x  e.  z }  e.  Fin ) )
92 simprl 755 . . . . . . . . . . . . . . . . . . . . 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_ 
ran  ( p  e.  a  |->  ( s  u.  p ) ) )
93 elun1 3630 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  s  ->  x  e.  ( s  u.  p
) )
9493ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  ( s  u.  p ) )
9594ralrimivw 2830 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 2899 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. p  e.  a  ( s  u.  p )  e.  _V
97 eleq2 2527 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  ( s  u.  p )  ->  (
x  e.  z  <->  x  e.  ( s  u.  p
) ) )
9861, 97ralrnmpt 5960 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. z  e.  ran  ( p  e.  a  |->  ( s  u.  p ) ) x  e.  z  <->  A. p  e.  a  x  e.  ( s  u.  p
) )
10095, 99sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 465 . . . . . . . . . . . . . . . . . . . . 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.  ran  ( p  e.  a  |->  ( s  u.  p ) ) x  e.  z )
102 ssralv 3523 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 60 . . . . . . . . . . . . . . . . . . . 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. z  e.  d  x  e.  z )
104 rabid2 3002 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  { z  e.  d  |  x  e.  z }  <->  A. z  e.  d  x  e.  z )
105103, 104sylibr 212 . . . . . . . . . . . . . . . . . . 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  =  { z  e.  d  |  x  e.  z } )
106105eleq1d 2523 . . . . . . . . . . . . . . . . . 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  <->  { z  e.  d  |  x  e.  z }  e.  Fin ) )
107106biimprd 223 . . . . . . . . . . . . . . . . 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
) )  ->  ( { z  e.  d  |  x  e.  z }  e.  Fin  ->  d  e.  Fin ) )
10861rnmpt 5192 . . . . . . . . . . . . . . . . . . . . 21  |-  ran  (
p  e.  a  |->  ( s  u.  p ) )  =  { q  |  E. p  e.  a  q  =  ( s  u.  p ) }
10992, 108syl6sseq 3509 . . . . . . . . . . . . . . . . . . . 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  C_ 
{ q  |  E. p  e.  a  q  =  ( s  u.  p ) } )
110 ssabral 3530 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 196 . . . . . . . . . . . . . . . . . . 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
) )  ->  A. q  e.  d  E. p  e.  a  q  =  ( s  u.  p
) )
112 uneq2 3611 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  =  ( f `  q )  ->  (
s  u.  p )  =  ( s  u.  ( f `  q
) ) )
113112eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  =  ( f `  q )  ->  (
q  =  ( s  u.  p )  <->  q  =  ( s  u.  (
f `  q )
) ) )
114113ac6sfi 7666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 435 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 16 . . . . . . . . . . . . . . . . . 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. f ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `  q
) ) ) ) )
117 frn 5672 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : d --> a  ->  ran  f  C_  a )
118117adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `
 q ) ) )  ->  ran  f  C_  a )
119118ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . 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  C_  a )
12034ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 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  e.  a )
121120snssd 4125 . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )  ->  { s } 
C_  a )
122119, 121unssd 3639 . . . . . . . . . . . . . . . . . . . . . . 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 } ) 
C_  a )
123 simprl 755 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )  ->  d  e.  Fin )
124 simprrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 : d --> a )
125 ffn 5666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : d --> a  -> 
f  Fn  d )
126124, 125syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 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  Fn  d
)
127 dffn4 5733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  Fn  d  <->  f :
d -onto-> ran  f )
128126, 127sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )  ->  f : d
-onto->
ran  f )
129 fofi 7707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  Fin  /\  f : d -onto-> ran  f
)  ->  ran  f  e. 
Fin )
130123, 128, 129syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 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  e.  Fin )
131 snfi 7499 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { s }  e.  Fin
132 unfi 7689 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  f  e.  Fin  /\ 
{ s }  e.  Fin )  ->  ( ran  f  u.  { s } )  e.  Fin )
133130, 131, 132sylancl 662 . . . . . . . . . . . . . . . . . . . . . . 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.  Fin )
134 elfpw 7723 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 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 664 . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )  ->  ( ran  f  u.  { s } )  e.  ( ~P a  i^i  Fin ) )
136 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . . 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. d )
137 uniiun 4330 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U. d  =  U_ q  e.  d  q
138 simprrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . 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. q  e.  d  q  =  ( s  u.  ( f `  q ) ) )
139 iuneq2 4294 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A. q  e.  d  q  =  ( s  u.  ( f `  q
) )  ->  U_ q  e.  d  q  =  U_ q  e.  d  ( s  u.  ( f `
 q ) ) )
140138, 139syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 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_ q  e.  d  q  =  U_ q  e.  d  ( s  u.  ( f `  q
) ) )
141137, 140syl5eq 2507 . . . . . . . . . . . . . . . . . . . . . . . . 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. d  =  U_ q  e.  d  (
s  u.  ( f `
 q ) ) )
142136, 141eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . 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  =  U_ q  e.  d  (
s  u.  ( f `
 q ) ) )
143 ssun2 3627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  { s }  C_  ( ran  f  u.  { s } )
144 ssnid 4013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  s  e. 
{ s }
145143, 144sselii 3460 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  s  e.  ( ran  f  u. 
{ s } )
146 elssuni 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( ran  f  u.  { s } )  ->  s  C_  U. ( ran  f  u.  { s } ) )
147145, 146ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  s  C_  U. ( ran  f  u. 
{ s } )
148 fvssunirn 5821 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f `
 q )  C_  U.
ran  f
149 ssun1 3626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ran  f  C_  ( ran  f  u. 
{ s } )
150149unissi 4221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  U. ran  f  C_  U. ( ran  f  u.  { s } )
151148, 150sstri 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 q )  C_  U. ( ran  f  u. 
{ s } )
152147, 151unssi 3638 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  u.  ( f `  q ) )  C_  U. ( ran  f  u. 
{ s } )
153152rgenw 2899 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  A. q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
154 iunss 4318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 } ) )
155153, 154mpbir 209 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U_ q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
156142, 155syl6eqss 3513 . . . . . . . . . . . . . . . . . . . . . . 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  C_  U. ( ran  f  u.  { s } ) )
15733ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )  ->  a  C_  J
)
158119, 157sstrd 3473 . . . . . . . . . . . . . . . . . . . . . . . . 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_  J )
15935ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 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.  J
)
160159snssd 4125 . . . . . . . . . . . . . . . . . . . . . . . . 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_  J )
161158, 160unssd 3639 . . . . . . . . . . . . . . . . . . . . . . . 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_  J )
162 uniss 4219 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ran  f  u.  {
s } )  C_  J  ->  U. ( ran  f  u.  { s } ) 
C_  U. J )
163162, 2syl6sseqr 3510 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  f  u.  {
s } )  C_  J  ->  U. ( ran  f  u.  { s } ) 
C_  X )
164161, 163syl 16 . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )  ->  U. ( ran  f  u.  { s } ) 
C_  X )
165156, 164eqssd 3480 . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )  ->  X  =  U. ( ran  f  u.  {
s } ) )
166 unieq 4206 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  ( ran  f  u.  { s } )  ->  U. b  =  U. ( ran  f  u.  {
s } ) )
167166eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  ( ran  f  u.  { s } )  ->  ( X  = 
U. b  <->  X  =  U. ( ran  f  u. 
{ s } ) ) )
168167rspcev 3177 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 )
169135, 165, 168syl2anc 661 . . . . . . . . . . . . . . . . . . . . 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 )
170169expr 615 . . . . . . . . . . . . . . . . . . . 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 )  ->  (
( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  (
f `  q )
) )  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b ) )
171170exlimdv 1691 . . . . . . . . . . . . . . . . . . 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
) )
172171ex 434 . . . . . . . . . . . . . . . . . 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. f ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `  q
) ) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
173116, 172mpdd 40 . . . . . . . . . . . . . . . . 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.  Fin  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) )
17491, 107, 1733syld 55 . . . . . . . . . . . . . . . 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 ) )
175174ex 434 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) )
176175com23 78 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) )
177176rexlimdv 2944 . . . . . . . . . . . . 13  |-  ( ( ( 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
) )
17877, 177syld 44 . . . . . . . . . . . 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 ) )
179178rexlimdvaa 2946 . . . . . . . . . . 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 ) ) )
18032, 179syld 44 . . . . . . . . . 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 ) ) )
181180exlimdv 1691 . . . . . . . . 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
) ) )
18227, 181syl5bi 217 . . . . . . . 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 ) ) )
18326, 182pm2.61dne 2768 . . . . . . 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 ) )
18415, 183syl3an3 1254 . . . . . 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
) )
1851843exp 1187 . . . . 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 ) ) ) )
186185com24 87 . . . 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 ) ) ) )
187186ralrimdv 2909 . . 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 ) ) )
1882iscmp 19122 . . . 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
) ) )
189188baibr 897 . . 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 ) )
190187, 189sylibd 214 . 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 ) )
19114, 190impbid2 204 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370   E.wex 1587    e. wcel 1758   {cab 2439    =/= wne 2647   A.wral 2798   E.wrex 2799   {crab 2802   _Vcvv 3076    u. cun 3433    i^i cin 3434    C_ wss 3435   (/)c0 3744   ~Pcpw 3967   {csn 3984   U.cuni 4198   U_ciun 4278    |-> cmpt 4457   ran crn 4948    Fn wfn 5520   -->wf 5521   -onto->wfo 5523   ` cfv 5525   Fincfn 7419   Topctop 18629   Compccmp 19120   PtFincptfin 28680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-om 6586  df-recs 6941  df-rdg 6975  df-1o 7029  df-oadd 7033  df-er 7210  df-en 7420  df-dom 7421  df-fin 7423  df-top 18634  df-cmp 19121  df-ptfin 28684
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator