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

Theorem comppfsc 26079
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 3751 . . . 4  |-  ( c  e.  ~P J  -> 
c  C_  J )
2 comppfsc.1 . . . . . . 7  |-  X  = 
U. J
32cmpcov 17375 . . . . . 6  |-  ( ( J  e.  Comp  /\  c  C_  J  /\  X  = 
U. c )  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)
4 elfpw 7344 . . . . . . . 8  |-  ( d  e.  ( ~P c  i^i  Fin )  <->  ( d  C_  c  /\  d  e. 
Fin ) )
5 finptfin 26069 . . . . . . . . . . 11  |-  ( d  e.  Fin  ->  d  e.  PtFin )
65anim1i 552 . . . . . . . . . 10  |-  ( ( d  e.  Fin  /\  ( d  C_  c  /\  X  =  U. d ) )  -> 
( d  e.  PtFin  /\  ( d  C_  c  /\  X  =  U. d ) ) )
76anassrs 630 . . . . . . . . 9  |-  ( ( ( d  e.  Fin  /\  d  C_  c )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
87ancom1s 781 . . . . . . . 8  |-  ( ( ( d  C_  c  /\  d  e.  Fin )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
94, 8sylanb 459 . . . . . . 7  |-  ( ( d  e.  ( ~P c  i^i  Fin )  /\  X  =  U. d )  ->  (
d  e.  PtFin  /\  (
d  C_  c  /\  X  =  U. d
) ) )
109reximi2 2756 . . . . . 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 1152 . . . 4  |-  ( J  e.  Comp  ->  ( c 
C_  J  ->  ( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) ) ) )
131, 12syl5 30 . . 3  |-  ( J  e.  Comp  ->  ( c  e.  ~P J  -> 
( X  =  U. c  ->  E. d  e.  PtFin  ( d  C_  c  /\  X  =  U. d
) ) ) )
1413ralrimiv 2732 . 2  |-  ( J  e.  Comp  ->  A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) ) )
15 elpwi 3751 . . . . . . 7  |-  ( a  e.  ~P J  -> 
a  C_  J )
16 0elpw 4311 . . . . . . . . . . 11  |-  (/)  e.  ~P a
17 0fin 7273 . . . . . . . . . . 11  |-  (/)  e.  Fin
18 elin 3474 . . . . . . . . . . 11  |-  ( (/)  e.  ( ~P a  i^i 
Fin )  <->  ( (/)  e.  ~P a  /\  (/)  e.  Fin )
)
1916, 17, 18mpbir2an 887 . . . . . . . . . 10  |-  (/)  e.  ( ~P a  i^i  Fin )
20 unieq 3967 . . . . . . . . . . . . 13  |-  ( b  =  (/)  ->  U. b  =  U. (/) )
21 uni0 3985 . . . . . . . . . . . . 13  |-  U. (/)  =  (/)
2220, 21syl6eq 2436 . . . . . . . . . . . 12  |-  ( b  =  (/)  ->  U. b  =  (/) )
2322eqeq2d 2399 . . . . . . . . . . 11  |-  ( b  =  (/)  ->  ( X  =  U. b  <->  X  =  (/) ) )
2423rspcev 2996 . . . . . . . . . 10  |-  ( (
(/)  e.  ( ~P a  i^i  Fin )  /\  X  =  (/) )  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
)
2519, 24mpan 652 . . . . . . . . 9  |-  ( X  =  (/)  ->  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b )
2625a1i13 25990 . . . . . . . 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 3581 . . . . . . . . 9  |-  ( X  =/=  (/)  <->  E. x  x  e.  X )
28 simp2 958 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  X  =  U. a )
2928eleq2d 2455 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  <->  x  e.  U. a
) )
3029biimpd 199 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  ->  x  e.  U. a ) )
31 eluni2 3962 . . . . . . . . . . . 12  |-  ( x  e.  U. a  <->  E. s  e.  a  x  e.  s )
3230, 31syl6ib 218 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  ( x  e.  X  ->  E. s  e.  a  x  e.  s ) )
33 simpl3 962 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
a  C_  J )
34 simprl 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  a )
3533, 34sseldd 3293 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
36 elssuni 3986 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  J  ->  s  C_ 
U. J )
3736, 2syl6sseqr 3339 . . . . . . . . . . . . . . . . . . . 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 2734 . . . . . . . . . . . . . . . . . 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 4074 . . . . . . . . . . . . . . . . . 18  |-  ( U_ p  e.  a  s  C_  X  <->  A. p  e.  a  s  C_  X )
4139, 40sylibr 204 . . . . . . . . . . . . . . . . 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 3461 . . . . . . . . . . . . . . . . 17  |-  ( U_ p  e.  a  s  C_  X  <->  ( U_ p  e.  a  s  u.  X )  =  X )
4341, 42sylib 189 . . . . . . . . . . . . . . . 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 961 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U. a
)
45 uniiun 4086 . . . . . . . . . . . . . . . . . 18  |-  U. a  =  U_ p  e.  a  p
4644, 45syl6eq 2436 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U_ p  e.  a  p )
4746uneq2d 3445 . . . . . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . . 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 4113 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  (
U_ p  e.  a  s  u.  U_ p  e.  a  p )
50 vex 2903 . . . . . . . . . . . . . . . . . 18  |-  s  e. 
_V
51 vex 2903 . . . . . . . . . . . . . . . . . 18  |-  p  e. 
_V
5250, 51unex 4648 . . . . . . . . . . . . . . . . 17  |-  ( s  u.  p )  e. 
_V
5352dfiun3 5065 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5449, 53eqtr3i 2410 . . . . . . . . . . . . . . 15  |-  ( U_ p  e.  a  s  u.  U_ p  e.  a  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5548, 54syl6eq 2436 . . . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  J  e.  Top )
5735adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  s  e.  J )
5833sselda 3292 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  p  e.  J )
59 unopn 16900 . . . . . . . . . . . . . . . . . . 19  |-  ( ( J  e.  Top  /\  s  e.  J  /\  p  e.  J )  ->  ( s  u.  p
)  e.  J )
6056, 57, 58, 59syl3anc 1184 . . . . . . . . . . . . . . . . . 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 2388 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  a  |->  ( s  u.  p ) )  =  ( p  e.  a  |->  ( s  u.  p ) )
6260, 61fmptd 5833 . . . . . . . . . . . . . . . . 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 5538 . . . . . . . . . . . . . . . . 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 4305 . . . . . . . . . . . . . . . . . 18  |-  ( J  e.  Top  ->  ( ran  ( p  e.  a 
|->  ( s  u.  p
) )  e.  ~P J 
<->  ran  ( p  e.  a  |->  ( s  u.  p ) )  C_  J ) )
66653ad2ant1 978 . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . 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 224 . . . . . . . . . . . . . . 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 3967 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  U. c  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) ) )
7069eqeq2d 2399 . . . . . . . . . . . . . . . . 17  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( X  = 
U. c  <->  X  =  U. ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
71 sseq2 3314 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( d  C_  c 
<->  d  C_  ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
7271anbi1d 686 . . . . . . . . . . . . . . . . . 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 2671 . . . . . . . . . . . . . . . . 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 312 . . . . . . . . . . . . . . . 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 2992 . . . . . . . . . . . . . . 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 39 . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  s )
79 ssel2 3287 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  C_  J  /\  s  e.  a )  ->  s  e.  J )
80793ad2antl3 1121 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  s  e.  a )  ->  s  e.  J )
8180adantrr 698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
82 elunii 3963 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  s  /\  s  e.  J )  ->  x  e.  U. J
)
8378, 81, 82syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  U. J )
8483, 2syl6eleqr 2479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  X )
8584adantr 452 . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . 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 2388 . . . . . . . . . . . . . . . . . . . 20  |-  U. d  =  U. d
8988ptfinfin 26070 . . . . . . . . . . . . . . . . . . 19  |-  ( ( d  e.  PtFin  /\  x  e.  U. d )  ->  { z  e.  d  |  x  e.  z }  e.  Fin )
9089expcom 425 . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . 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 3458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  s  ->  x  e.  ( s  u.  p
) )
9493ad2antll 710 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  x  e.  ( s  u.  p ) )
9594ralrimivw 2734 . . . . . . . . . . . . . . . . . . . . . . 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 2717 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. p  e.  a  ( s  u.  p )  e.  _V
97 eleq2 2449 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  ( s  u.  p )  ->  (
x  e.  z  <->  x  e.  ( s  u.  p
) ) )
9861, 97ralrnmpt 5818 . . . . . . . . . . . . . . . . . . . . . . . 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 8 . . . . . . . . . . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . . . . . . . . . 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 58 . . . . . . . . . . . . . . . . . . . 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 2829 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  { z  e.  d  |  x  e.  z }  <->  A. z  e.  d  x  e.  z )
105103, 104sylibr 204 . . . . . . . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . 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 5057 . . . . . . . . . . . . . . . . . . . . 21  |-  ran  (
p  e.  a  |->  ( s  u.  p ) )  =  { q  |  E. p  e.  a  q  =  ( s  u.  p ) }
10992, 108syl6sseq 3338 . . . . . . . . . . . . . . . . . . . 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 3358 . . . . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . . . . 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 3439 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  =  ( f `  q )  ->  (
s  u.  p )  =  ( s  u.  ( f `  q
) ) )
113112eqeq2d 2399 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  =  ( f `  q )  ->  (
q  =  ( s  u.  p )  <->  q  =  ( s  u.  (
f `  q )
) ) )
114113ac6sfi 7288 . . . . . . . . . . . . . . . . . . . 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 425 . . . . . . . . . . . . . . . . . . 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 5538 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : d --> a  ->  ran  f  C_  a )
118117adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f : d --> a  /\  A. q  e.  d  q  =  ( s  u.  ( f `
 q ) ) )  ->  ran  f  C_  a )
119118ad2antll 710 . . . . . . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . . . . . 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 3887 . . . . . . . . . . . . . . . . . . . . . . . 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 3467 . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5532 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5600 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  Fn  d  <->  f :
d -onto-> ran  f )
128126, 127sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . 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 7329 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  Fin  /\  f : d -onto-> ran  f
)  ->  ran  f  e. 
Fin )
130123, 128, 129syl2anc 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  e.  Fin )
131 snfi 7124 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { s }  e.  Fin
132 unfi 7311 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  f  e.  Fin  /\ 
{ s }  e.  Fin )  ->  ( ran  f  u.  { s } )  e.  Fin )
133130, 131, 132sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 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 7344 . . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . . . . . . . . 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 4086 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U. d  =  U_ q  e.  d  q
138 simprrr 742 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4052 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2432 . . . . . . . . . . . . . . . . . . . . . . . . 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 2420 . . . . . . . . . . . . . . . . . . . . . . . 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 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  { s }  C_  ( ran  f  u.  { s } )
14450snid 3785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  s  e. 
{ s }
145143, 144sselii 3289 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  s  e.  ( ran  f  u. 
{ s } )
146 elssuni 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( ran  f  u.  { s } )  ->  s  C_  U. ( ran  f  u.  { s } ) )
147145, 146ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  s  C_  U. ( ran  f  u. 
{ s } )
148 fvssunirn 5695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f `
 q )  C_  U.
ran  f
149 ssun1 3454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ran  f  C_  ( ran  f  u. 
{ s } )
150149unissi 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  U. ran  f  C_  U. ( ran  f  u.  { s } )
151148, 150sstri 3301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 q )  C_  U. ( ran  f  u. 
{ s } )
152147, 151unssi 3466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  u.  ( f `  q ) )  C_  U. ( ran  f  u. 
{ s } )
153152rgenw 2717 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  A. q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
154 iunss 4074 . . . . . . . . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U_ q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
156142, 155syl6eqss 3342 . . . . . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3302 . . . . . . . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3887 . . . . . . . . . . . . . . . . . . . . . . . . 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 3467 . . . . . . . . . . . . . . . . . . . . . . . 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 3979 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ran  f  u.  {
s } )  C_  J  ->  U. ( ran  f  u.  { s } ) 
C_  U. J )
163162, 2syl6sseqr 3339 . . . . . . . . . . . . . . . . . . . . . . . 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 3309 . . . . . . . . . . . . . . . . . . . . . 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 3967 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  ( ran  f  u.  { s } )  ->  U. b  =  U. ( ran  f  u.  {
s } ) )
167166eqeq2d 2399 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  ( ran  f  u.  { s } )  ->  ( X  = 
U. b  <->  X  =  U. ( ran  f  u. 
{ s } ) ) )
168167rspcev 2996 . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . 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 599 . . . . . . . . . . . . . . . . . . . 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 1643 . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . 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 38 . . . . . . . . . . . . . . . . 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 53 . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . 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 74 . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . 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 42 . . . . . . . . . . . 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 2775 . . . . . . . . . . 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 42 . . . . . . . . . 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 1643 . . . . . . . . 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 209 . . . . . . . 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 2628 . . . . . . 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 1219 . . . . . 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 1152 . . . . 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 83 . . . 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 2739 . . 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 17374 . . . 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 873 . . 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 206 . 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 196 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 177    /\ wa 359    /\ w3a 936   E.wex 1547    = wceq 1649    e. wcel 1717   {cab 2374    =/= wne 2551   A.wral 2650   E.wrex 2651   {crab 2654   _Vcvv 2900    u. cun 3262    i^i cin 3263    C_ wss 3264   (/)c0 3572   ~Pcpw 3743   {csn 3758   U.cuni 3958   U_ciun 4036    e. cmpt 4208   ran crn 4820    Fn wfn 5390   -->wf 5391   -onto->wfo 5393   ` cfv 5395   Fincfn 7046   Topctop 16882   Compccmp 17372   PtFincptfin 26033
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-reu 2657  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-int 3994  df-iun 4038  df-br 4155  df-opab 4209  df-mpt 4210  df-tr 4245  df-eprel 4436  df-id 4440  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-lim 4528  df-suc 4529  df-om 4787  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-ov 6024  df-oprab 6025  df-mpt2 6026  df-recs 6570  df-rdg 6605  df-1o 6661  df-oadd 6665  df-er 6842  df-en 7047  df-dom 7048  df-fin 7050  df-top 16887  df-cmp 17373  df-ptfin 26037
  Copyright terms: Public domain W3C validator