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

Theorem comppfsc 26341
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 3799 . . . 4  |-  ( c  e.  ~P J  -> 
c  C_  J )
2 comppfsc.1 . . . . . . 7  |-  X  = 
U. J
32cmpcov 17442 . . . . . 6  |-  ( ( J  e.  Comp  /\  c  C_  J  /\  X  = 
U. c )  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)
4 elfpw 7400 . . . . . . . 8  |-  ( d  e.  ( ~P c  i^i  Fin )  <->  ( d  C_  c  /\  d  e. 
Fin ) )
5 finptfin 26331 . . . . . . . . . . 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 2804 . . . . . 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 2780 . 2  |-  ( J  e.  Comp  ->  A. c  e.  ~P  J ( X  =  U. c  ->  E. d  e.  PtFin  ( d 
C_  c  /\  X  =  U. d ) ) )
15 elpwi 3799 . . . . . . 7  |-  ( a  e.  ~P J  -> 
a  C_  J )
16 0elpw 4361 . . . . . . . . . . 11  |-  (/)  e.  ~P a
17 0fin 7328 . . . . . . . . . . 11  |-  (/)  e.  Fin
18 elin 3522 . . . . . . . . . . 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 4016 . . . . . . . . . . . . 13  |-  ( b  =  (/)  ->  U. b  =  U. (/) )
21 uni0 4034 . . . . . . . . . . . . 13  |-  U. (/)  =  (/)
2220, 21syl6eq 2483 . . . . . . . . . . . 12  |-  ( b  =  (/)  ->  U. b  =  (/) )
2322eqeq2d 2446 . . . . . . . . . . 11  |-  ( b  =  (/)  ->  ( X  =  U. b  <->  X  =  (/) ) )
2423rspcev 3044 . . . . . . . . . 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 26252 . . . . . . . 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 3629 . . . . . . . . 9  |-  ( X  =/=  (/)  <->  E. x  x  e.  X )
28 simp2 958 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  ->  X  =  U. a )
2928eleq2d 2502 . . . . . . . . . . . . 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 4011 . . . . . . . . . . . 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 3341 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  -> 
s  e.  J )
36 elssuni 4035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  J  ->  s  C_ 
U. J )
3736, 2syl6sseqr 3387 . . . . . . . . . . . . . . . . . . . 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 2782 . . . . . . . . . . . . . . . . . 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 4124 . . . . . . . . . . . . . . . . . 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 3509 . . . . . . . . . . . . . . . . 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 4136 . . . . . . . . . . . . . . . . . 18  |-  U. a  =  U_ p  e.  a  p
4644, 45syl6eq 2483 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  X  =  U. a  /\  a  C_  J )  /\  ( s  e.  a  /\  x  e.  s ) )  ->  X  =  U_ p  e.  a  p )
4746uneq2d 3493 . . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . . 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 4163 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  (
U_ p  e.  a  s  u.  U_ p  e.  a  p )
50 vex 2951 . . . . . . . . . . . . . . . . . 18  |-  s  e. 
_V
51 vex 2951 . . . . . . . . . . . . . . . . . 18  |-  p  e. 
_V
5250, 51unex 4699 . . . . . . . . . . . . . . . . 17  |-  ( s  u.  p )  e. 
_V
5352dfiun3 5116 . . . . . . . . . . . . . . . 16  |-  U_ p  e.  a  ( s  u.  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5449, 53eqtr3i 2457 . . . . . . . . . . . . . . 15  |-  ( U_ p  e.  a  s  u.  U_ p  e.  a  p )  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) )
5548, 54syl6eq 2483 . . . . . . . . . . . . . 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 3340 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( J  e. 
Top  /\  X  =  U. a  /\  a  C_  J )  /\  (
s  e.  a  /\  x  e.  s )
)  /\  p  e.  a )  ->  p  e.  J )
59 unopn 16966 . . . . . . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  a  |->  ( s  u.  p ) )  =  ( p  e.  a  |->  ( s  u.  p ) )
6260, 61fmptd 5885 . . . . . . . . . . . . . . . . 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 5589 . . . . . . . . . . . . . . . . 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 4355 . . . . . . . . . . . . . . . . . 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 4016 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  U. c  =  U. ran  ( p  e.  a 
|->  ( s  u.  p
) ) )
7069eqeq2d 2446 . . . . . . . . . . . . . . . . 17  |-  ( c  =  ran  ( p  e.  a  |->  ( s  u.  p ) )  ->  ( X  = 
U. c  <->  X  =  U. ran  ( p  e.  a  |->  ( s  u.  p ) ) ) )
71 sseq2 3362 . . . . . . . . . . . . . . . . . . 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 2718 . . . . . . . . . . . . . . . . 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 3040 . . . . . . . . . . . . . . 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 3335 . . . . . . . . . . . . . . . . . . . . . . . 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 4012 . . . . . . . . . . . . . . . . . . . . . 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 2526 . . . . . . . . . . . . . . . . . . . 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 2511 . . . . . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . . . . . . . 20  |-  U. d  =  U. d
8988ptfinfin 26332 . . . . . . . . . . . . . . . . . . 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 3506 . . . . . . . . . . . . . . . . . . . . . . . . 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 2782 . . . . . . . . . . . . . . . . . . . . . . 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 2765 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. p  e.  a  ( s  u.  p )  e.  _V
97 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  ( s  u.  p )  ->  (
x  e.  z  <->  x  e.  ( s  u.  p
) ) )
9861, 97ralrnmpt 5870 . . . . . . . . . . . . . . . . . . . . . . . 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 3399 . . . . . . . . . . . . . . . . . . . . 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 2877 . . . . . . . . . . . . . . . . . . . 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 2501 . . . . . . . . . . . . . . . . . 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 5108 . . . . . . . . . . . . . . . . . . . . 21  |-  ran  (
p  e.  a  |->  ( s  u.  p ) )  =  { q  |  E. p  e.  a  q  =  ( s  u.  p ) }
10992, 108syl6sseq 3386 . . . . . . . . . . . . . . . . . . . 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 3406 . . . . . . . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  =  ( f `  q )  ->  (
s  u.  p )  =  ( s  u.  ( f `  q
) ) )
113112eqeq2d 2446 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  =  ( f `  q )  ->  (
q  =  ( s  u.  p )  <->  q  =  ( s  u.  (
f `  q )
) ) )
114113ac6sfi 7343 . . . . . . . . . . . . . . . . . . . 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 5589 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3935 . . . . . . . . . . . . . . . . . . . . . . . 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 3515 . . . . . . . . . . . . . . . . . . . . . . 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 5583 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5651 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7384 . . . . . . . . . . . . . . . . . . . . . . . . 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 7179 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { s }  e.  Fin
132 unfi 7366 . . . . . . . . . . . . . . . . . . . . . . . 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 7400 . . . . . . . . . . . . . . . . . . . . . . 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 4136 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4101 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . . . . . . 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 3503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  { s }  C_  ( ran  f  u.  { s } )
14450snid 3833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  s  e. 
{ s }
145143, 144sselii 3337 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  s  e.  ( ran  f  u. 
{ s } )
146 elssuni 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5746 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f `
 q )  C_  U.
ran  f
149 ssun1 3502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ran  f  C_  ( ran  f  u. 
{ s } )
150149unissi 4030 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  U. ran  f  C_  U. ( ran  f  u.  { s } )
151148, 150sstri 3349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 q )  C_  U. ( ran  f  u. 
{ s } )
152147, 151unssi 3514 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  u.  ( f `  q ) )  C_  U. ( ran  f  u. 
{ s } )
153152rgenw 2765 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  A. q  e.  d  ( s  u.  ( f `  q
) )  C_  U. ( ran  f  u.  { s } )
154 iunss 4124 . . . . . . . . . . . . . . . . . . . . . . . . 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 3390 . . . . . . . . . . . . . . . . . . . . . . 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 3350 . . . . . . . . . . . . . . . . . . . . . . . . 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 3935 . . . . . . . . . . . . . . . . . . . . . . . . 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 3515 . . . . . . . . . . . . . . . . . . . . . . . 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 4028 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ran  f  u.  {
s } )  C_  J  ->  U. ( ran  f  u.  { s } ) 
C_  U. J )
163162, 2syl6sseqr 3387 . . . . . . . . . . . . . . . . . . . . . . . 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 3357 . . . . . . . . . . . . . . . . . . . . . 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 4016 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  ( ran  f  u.  { s } )  ->  U. b  =  U. ( ran  f  u.  {
s } ) )
167166eqeq2d 2446 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  ( ran  f  u.  { s } )  ->  ( X  = 
U. b  <->  X  =  U. ( ran  f  u. 
{ s } ) ) )
168167rspcev 3044 . . . . . . . . . . . . . . . . . . . . . 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 1646 . . . . . . . . . . . . . . . . . . 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 2821 . . . . . . . . . . . . 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 2823 . . . . . . . . . . 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 1646 . . . . . . . . 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 2675 . . . . . . 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 2787 . . 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 17441 . . . 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 1550    = wceq 1652    e. wcel 1725   {cab 2421    =/= wne 2598   A.wral 2697   E.wrex 2698   {crab 2701   _Vcvv 2948    u. cun 3310    i^i cin 3311    C_ wss 3312   (/)c0 3620   ~Pcpw 3791   {csn 3806   U.cuni 4007   U_ciun 4085    e. cmpt 4258   ran crn 4871    Fn wfn 5441   -->wf 5442   -onto->wfo 5444   ` cfv 5446   Fincfn 7101   Topctop 16948   Compccmp 17439   PtFincptfin 26295
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-recs 6625  df-rdg 6660  df-1o 6716  df-oadd 6720  df-er 6897  df-en 7102  df-dom 7103  df-fin 7105  df-top 16953  df-cmp 17440  df-ptfin 26299
  Copyright terms: Public domain W3C validator