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

Theorem comppfsc 28532
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 3864 . . . 4  |-  ( c  e.  ~P J  -> 
c  C_  J )
2 comppfsc.1 . . . . . . 7  |-  X  = 
U. J
32cmpcov 18967 . . . . . 6  |-  ( ( J  e.  Comp  /\  c  C_  J  /\  X  = 
U. c )  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)
4 elfpw 7605 . . . . . . . 8  |-  ( d  e.  ( ~P c  i^i  Fin )  <->  ( d  C_  c  /\  d  e. 
Fin ) )
5 finptfin 28522 . . . . . . . . . . 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 2817 . . . . . 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 1186 . . . 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 2793 . 2  |-  ( J  e.  Comp  ->  A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) ) )
15 elpwi 3864 . . . . . . 7  |-  ( a  e.  ~P J  -> 
a  C_  J )
16 0elpw 4456 . . . . . . . . . . 11  |-  (/)  e.  ~P a
17 0fin 7532 . . . . . . . . . . 11  |-  (/)  e.  Fin
18 elin 3534 . . . . . . . . . . 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 4094 . . . . . . . . . . . . 13  |-  ( b  =  (/)  ->  U. b  =  U. (/) )
21 uni0 4113 . . . . . . . . . . . . 13  |-  U. (/)  =  (/)
2220, 21syl6eq 2486 . . . . . . . . . . . 12  |-  ( b  =  (/)  ->  U. b  =  (/) )
2322eqeq2d 2449 . . . . . . . . . . 11  |-  ( b  =  (/)  ->  ( X  =  U. b  <->  X  =  (/) ) )
2423rspcev 3068 . . . . . . . . . 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 28443 . . . . . . . 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 3641 . . . . . . . . 9  |-  ( X  =/=  (/)  <->  E. x  x  e.  X )
28 simp2 989 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  X  =  U. a )
2928eleq2d 2505 . . . . . . . . . . . . 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 4090 . . . . . . . . . . . 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 3352 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
36 elssuni 4116 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  J  ->  s  C_ 
U. J )
3736, 2syl6sseqr 3398 . . . . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . . . . 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 4206 . . . . . . . . . . . . . . . . . 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 3521 . . . . . . . . . . . . . . . . 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 4218 . . . . . . . . . . . . . . . . . 18  |-  U. a  =  U_ p  e.  a  p
4644, 45syl6eq 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U_ p  e.  a  p )
4746uneq2d 3505 . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . 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 4246 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  (
U_ p  e.  a  s  u.  U_ p  e.  a  p )
50 vex 2970 . . . . . . . . . . . . . . . . . 18  |-  s  e. 
_V
51 vex 2970 . . . . . . . . . . . . . . . . . 18  |-  p  e. 
_V
5250, 51unex 6373 . . . . . . . . . . . . . . . . 17  |-  ( s  u.  p )  e. 
_V
5352dfiun3 5089 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5449, 53eqtr3i 2460 . . . . . . . . . . . . . . 15  |-  ( U_ p  e.  a  s  u.  U_ p  e.  a  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5548, 54syl6eq 2486 . . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  p  e.  J )
59 unopn 18491 . . . . . . . . . . . . . . . . . . 19  |-  ( ( J  e.  Top  /\  s  e.  J  /\  p  e.  J )  ->  ( s  u.  p
)  e.  J )
6056, 57, 58, 59syl3anc 1218 . . . . . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  a  |->  ( s  u.  p ) )  =  ( p  e.  a  |->  ( s  u.  p ) )
6260, 61fmptd 5862 . . . . . . . . . . . . . . . . 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 5560 . . . . . . . . . . . . . . . . 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 4450 . . . . . . . . . . . . . . . . . 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 4094 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  U. c  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) ) )
7069eqeq2d 2449 . . . . . . . . . . . . . . . . 17  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( X  = 
U. c  <->  X  =  U. ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
71 sseq2 3373 . . . . . . . . . . . . . . . . . . 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 2731 . . . . . . . . . . . . . . . . 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 3064 . . . . . . . . . . . . . . 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 3346 . . . . . . . . . . . . . . . . . . . . . . . 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 4091 . . . . . . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . . 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 2514 . . . . . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . . . . . . 20  |-  U. d  =  U. d
8988ptfinfin 28523 . . . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . . . . . . . . . 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 2778 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. p  e.  a  ( s  u.  p )  e.  _V
97 eleq2 2499 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  ( s  u.  p )  ->  (
x  e.  z  <->  x  e.  ( s  u.  p
) ) )
9861, 97ralrnmpt 5847 . . . . . . . . . . . . . . . . . . . . . . . 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 3411 . . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . . . 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 2504 . . . . . . . . . . . . . . . . . 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 5080 . . . . . . . . . . . . . . . . . . . . 21  |-  ran  (
p  e.  a  |->  ( s  u.  p ) )  =  { q  |  E. p  e.  a  q  =  ( s  u.  p ) }
10992, 108syl6sseq 3397 . . . . . . . . . . . . . . . . . . . 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 3418 . . . . . . . . . . . . . . . . . . . 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 3499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  =  ( f `  q )  ->  (
s  u.  p )  =  ( s  u.  ( f `  q
) ) )
113112eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  =  ( f `  q )  ->  (
q  =  ( s  u.  p )  <->  q  =  ( s  u.  (
f `  q )
) ) )
114113ac6sfi 7548 . . . . . . . . . . . . . . . . . . . 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 5560 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4013 . . . . . . . . . . . . . . . . . . . . . . . 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 3527 . . . . . . . . . . . . . . . . . . . . . . 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 5554 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5621 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7589 . . . . . . . . . . . . . . . . . . . . . . . . 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 7382 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { s }  e.  Fin
132 unfi 7571 . . . . . . . . . . . . . . . . . . . . . . . 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 7605 . . . . . . . . . . . . . . . . . . . . . . 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 4218 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . . . . . 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 3515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  { s }  C_  ( ran  f  u.  { s } )
144 ssnid 3901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  s  e. 
{ s }
145143, 144sselii 3348 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  s  e.  ( ran  f  u. 
{ s } )
146 elssuni 4116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f `
 q )  C_  U.
ran  f
149 ssun1 3514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ran  f  C_  ( ran  f  u. 
{ s } )
150149unissi 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  U. ran  f  C_  U. ( ran  f  u.  { s } )
151148, 150sstri 3360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 q )  C_  U. ( ran  f  u. 
{ s } )
152147, 151unssi 3526 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  u.  ( f `  q ) )  C_  U. ( ran  f  u. 
{ s } )
153152rgenw 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  A. q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
154 iunss 4206 . . . . . . . . . . . . . . . . . . . . . . . . 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 3401 . . . . . . . . . . . . . . . . . . . . . . 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 3361 . . . . . . . . . . . . . . . . . . . . . . . . 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 4013 . . . . . . . . . . . . . . . . . . . . . . . . 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 3527 . . . . . . . . . . . . . . . . . . . . . . . 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 4107 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ran  f  u.  {
s } )  C_  J  ->  U. ( ran  f  u.  { s } ) 
C_  U. J )
163162, 2syl6sseqr 3398 . . . . . . . . . . . . . . . . . . . . . . . 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 3368 . . . . . . . . . . . . . . . . . . . . . 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 4094 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  ( ran  f  u.  { s } )  ->  U. b  =  U. ( ran  f  u.  {
s } ) )
167166eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  ( ran  f  u.  { s } )  ->  ( X  = 
U. b  <->  X  =  U. ( ran  f  u. 
{ s } ) ) )
168167rspcev 3068 . . . . . . . . . . . . . . . . . . . . . 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 1690 . . . . . . . . . . . . . . . . . . 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 2835 . . . . . . . . . . . . 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 2837 . . . . . . . . . . 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 1690 . . . . . . . . 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 2683 . . . . . . 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 1253 . . . . . 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 1186 . . . . 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 2800 . . 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 18966 . . . 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 1369   E.wex 1586    e. wcel 1756   {cab 2424    =/= wne 2601   A.wral 2710   E.wrex 2711   {crab 2714   _Vcvv 2967    u. cun 3321    i^i cin 3322    C_ wss 3323   (/)c0 3632   ~Pcpw 3855   {csn 3872   U.cuni 4086   U_ciun 4166    e. cmpt 4345   ran crn 4836    Fn wfn 5408   -->wf 5409   -onto->wfo 5411   ` cfv 5413   Fincfn 7302   Topctop 18473   Compccmp 18964   PtFincptfin 28486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-fin 7306  df-top 18478  df-cmp 18965  df-ptfin 28490
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator