MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  comppfsc Structured version   Visualization version   Unicode version
Theorem comppfsc 20559
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 3962 . . . 4 |- ( c e. ~P J -> c C_ J )
2 comppfsc.1 . . . . . . 7 |- X = U. J
32cmpcov 20416 . . . . . 6 |- ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
4 elfpw 7881 . . . . . . . 8 |- ( d e. ( ~P c i^i Fin ) <-> ( d C_ c /\ d e. Fin ) )
5 finptfin 20545 . . . . . . . . . . 11 |- ( d e. Fin -> d e. PtFin )
65anim1i 572 . . . . . . . . . 10 |- ( ( d e. Fin /\ ( d C_ c /\ X = U. d ) ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
76anassrs 654 . . . . . . . . 9 |- ( ( ( d e. Fin /\ d C_ c ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
87ancom1s 815 . . . . . . . 8 |- ( ( ( d C_ c /\ d e. Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
94, 8sylanb 475 . . . . . . 7 |- ( ( d e. ( ~P c i^i Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
109reximi2 2856 . . . . . 6 |- ( E. d e. ( ~P c i^i Fin ) X = U. d -> E. d e. PtFin ( d C_ c /\ X = U. d ) )
113, 10syl 17 . . . . 5 |- ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. PtFin ( d C_ c /\ X = U. d ) )
12113exp 1208 . . . 4 |- ( J e. Comp -> ( c C_ J -> ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )
131, 12syl5 33 . . 3 |- ( J e. Comp -> ( c e. ~P J -> ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )
1413ralrimiv 2802 . 2 |- ( J e. Comp -> A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) )
15 elpwi 3962 . . . . . . 7 |- ( a e. ~P J -> a C_ J )
16 0elpw 4575 . . . . . . . . . . . 12 |- (/) e. ~P a
17 0fin 7804 . . . . . . . . . . . 12 |- (/) e. Fin
18 elin 3619 . . . . . . . . . . . 12 |- ( (/) e. ( ~P a i^i Fin ) <-> ( (/) e. ~P a /\ (/) e. Fin ) )
1916, 17, 18mpbir2an 932 . . . . . . . . . . 11 |- (/) e. ( ~P a i^i Fin )
20 unieq 4209 . . . . . . . . . . . . . 14 |- ( b = (/) -> U. b = U. (/) )
21 uni0 4228 . . . . . . . . . . . . . 14 |- U. (/) = (/)
2220, 21syl6eq 2503 . . . . . . . . . . . . 13 |- ( b = (/) -> U. b = (/) )
2322eqeq2d 2463 . . . . . . . . . . . 12 |- ( b = (/) -> ( X = U. b <-> X = (/) ) )
2423rspcev 3152 . . . . . . . . . . 11 |- ( ( (/) e. ( ~P a i^i Fin ) /\ X = (/) ) -> E. b e. ( ~P a i^i Fin ) X = U. b )
2519, 24mpan 677 . . . . . . . . . 10 |- ( X = (/) -> E. b e. ( ~P a i^i Fin ) X = U. b )
2625a1d 26 . . . . . . . . 9 |- ( 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 ) )
2726a1i 11 . . . . . . . 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 ) ) )
28 n0 3743 . . . . . . . . 9 |- ( X =/= (/) <-> E. x x e. X )
29 simp2 1010 . . . . . . . . . . . . . 14 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> X = U. a )
3029eleq2d 2516 . . . . . . . . . . . . 13 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X <-> x e. U. a ) )
3130biimpd 211 . . . . . . . . . . . 12 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> x e. U. a ) )
32 eluni2 4205 . . . . . . . . . . . 12 |- ( x e. U. a <-> E. s e. a x e. s )
3331, 32syl6ib 230 . . . . . . . . . . 11 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> E. s e. a x e. s ) )
34 simpl3 1014 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> a C_ J )
35 simprl 765 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. a )
3634, 35sseldd 3435 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
37 elssuni 4230 . . . . . . . . . . . . . . . . . . . . 21 |- ( s e. J -> s C_ U. J )
3837, 2syl6sseqr 3481 . . . . . . . . . . . . . . . . . . . 20 |- ( s e. J -> s C_ X )
3936, 38syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s C_ X )
4039ralrimivw 2805 . . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> A. p e. a s C_ X )
41 iunss 4322 . . . . . . . . . . . . . . . . . 18 |- ( U_ p e. a s C_ X <-> A. p e. a s C_ X )
4240, 41sylibr 216 . . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> U_ p e. a s C_ X )
43 ssequn1 3606 . . . . . . . . . . . . . . . . 17 |- ( U_ p e. a s C_ X <-> ( U_ p e. a s u. X ) = X )
4442, 43sylib 200 . . . . . . . . . . . . . . . 16 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( U_ p e. a s u. X ) = X )
45 simpl2 1013 . . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U. a )
46 uniiun 4334 . . . . . . . . . . . . . . . . . 18 |- U. a = U_ p e. a p
4745, 46syl6eq 2503 . . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U_ p e. a p )
4847uneq2d 3590 . . . . . . . . . . . . . . . 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 ) )
4944, 48eqtr3d 2489 . . . . . . . . . . . . . . 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 ) )
50 iunun 4365 . . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = ( U_ p e. a s u. U_ p e. a p )
51 vex 3050 . . . . . . . . . . . . . . . . . 18 |- s e. _V
52 vex 3050 . . . . . . . . . . . . . . . . . 18 |- p e. _V
5351, 52unex 6594 . . . . . . . . . . . . . . . . 17 |- ( s u. p ) e. _V
5453dfiun3 5092 . . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = U. ran ( p e. a |-> ( s u. p ) )
5550, 54eqtr3i 2477 . . . . . . . . . . . . . . 15 |- ( U_ p e. a s u. U_ p e. a p ) = U. ran ( p e. a |-> ( s u. p ) )
5649, 55syl6eq 2503 . . . . . . . . . . . . . 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 ) ) )
57 simpll1 1048 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> J e. Top )
5836adantr 467 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> s e. J )
5934sselda 3434 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> p e. J )
60 unopn 19945 . . . . . . . . . . . . . . . . . . 19 |- ( ( J e. Top /\ s e. J /\ p e. J ) -> ( s u. p ) e. J )
6157, 58, 59, 60syl3anc 1269 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> ( s u. p ) e. J )
62 eqid 2453 . . . . . . . . . . . . . . . . . 18 |- ( p e. a |-> ( s u. p ) ) = ( p e. a |-> ( s u. p ) )
6361, 62fmptd 6051 . . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( p e. a |-> ( s u. p ) ) : a --> J )
64 frn 5740 . . . . . . . . . . . . . . . . 17 |- ( ( p e. a |-> ( s u. p ) ) : a --> J -> ran ( p e. a |-> ( s u. p ) ) C_ J )
6563, 64syl 17 . . . . . . . . . . . . . . . 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 )
66 elpw2g 4569 . . . . . . . . . . . . . . . . . 18 |- ( J e. Top -> ( ran ( p e. a |-> ( s u. p ) ) e. ~P J <-> ran ( p e. a |-> ( s u. p ) ) C_ J ) )
67663ad2ant1 1030 . . . . . . . . . . . . . . . . 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 ) )
6867adantr 467 . . . . . . . . . . . . . . . 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 ) )
6965, 68mpbird 236 . . . . . . . . . . . . . . 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 )
70 unieq 4209 . . . . . . . . . . . . . . . . . 18 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> U. c = U. ran ( p e. a |-> ( s u. p ) ) )
7170eqeq2d 2463 . . . . . . . . . . . . . . . . 17 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( X = U. c <-> X = U. ran ( p e. a |-> ( s u. p ) ) ) )
72 sseq2 3456 . . . . . . . . . . . . . . . . . . 19 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( d C_ c <-> d C_ ran ( p e. a |-> ( s u. p ) ) ) )
7372anbi1d 712 . . . . . . . . . . . . . . . . . 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 ) ) )
7473rexbidv 2903 . . . . . . . . . . . . . . . . 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 ) ) )
7571, 74imbi12d 322 . . . . . . . . . . . . . . . 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 ) ) ) )
7675rspcv 3148 . . . . . . . . . . . . . . 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 ) ) ) )
7769, 76syl 17 . . . . . . . . . . . . . 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 ) ) ) )
7856, 77mpid 42 . . . . . . . . . . . . 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 ) ) )
79 simprr 767 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. s )
80 ssel2 3429 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( a C_ J /\ s e. a ) -> s e. J )
81803ad2antl3 1173 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ s e. a ) -> s e. J )
8281adantrr 724 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
83 elunii 4206 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. s /\ s e. J ) -> x e. U. J )
8479, 82, 83syl2anc 667 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. U. J )
8584, 2syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. X )
8685adantr 467 . . . . . . . . . . . . . . . . . . 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 )
87 simprr 767 . . . . . . . . . . . . . . . . . . 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 )
8886, 87eleqtrd 2533 . . . . . . . . . . . . . . . . . 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 )
89 eqid 2453 . . . . . . . . . . . . . . . . . . . 20 |- U. d = U. d
9089ptfinfin 20546 . . . . . . . . . . . . . . . . . . 19 |- ( ( d e. PtFin /\ x e. U. d ) -> { z e. d | x e. z } e. Fin )
9190expcom 437 . . . . . . . . . . . . . . . . . 18 |- ( x e. U. d -> ( d e. PtFin -> { z e. d | x e. z } e. Fin ) )
9288, 91syl 17 . . . . . . . . . . . . . . . . 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 ) )
93 simprl 765 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
94 elun1 3603 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. s -> x e. ( s u. p ) )
9594ad2antll 736 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. ( s u. p ) )
9695ralrimivw 2805 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
9753rgenw 2751 . . . . . . . . . . . . . . . . . . . . . . . 24 |- A. p e. a ( s u. p ) e. _V
98 eleq2 2520 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = ( s u. p ) -> ( x e. z <-> x e. ( s u. p ) ) )
9962, 98ralrnmpt 6036 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
10097, 99ax-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 ) )
10196, 100sylibr 216 . . . . . . . . . . . . . . . . . . . . . 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 )
102101adantr 467 . . . . . . . . . . . . . . . . . . . . 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 )
103 ssralv 3495 . . . . . . . . . . . . . . . . . . . . 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 ) )
10493, 102, 103sylc 62 . . . . . . . . . . . . . . . . . . . 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 )
105 rabid2 2970 . . . . . . . . . . . . . . . . . . . 20 |- ( d = { z e. d | x e. z } <-> A. z e. d x e. z )
106104, 105sylibr 216 . . . . . . . . . . . . . . . . . . 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 } )
107106eleq1d 2515 . . . . . . . . . . . . . . . . . 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 ) )
108107biimprd 227 . . . . . . . . . . . . . . . . 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 ) )
10962rnmpt 5083 . . . . . . . . . . . . . . . . . . . . 21 |- ran ( p e. a |-> ( s u. p ) ) = { q | E. p e. a q = ( s u. p ) }
11093, 109syl6sseq 3480 . . . . . . . . . . . . . . . . . . . 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 ) } )
111 ssabral 3502 . . . . . . . . . . . . . . . . . . . 20 |- ( d C_ { q | E. p e. a q = ( s u. p ) } <-> A. q e. d E. p e. a q = ( s u. p ) )
112110, 111sylib 200 . . . . . . . . . . . . . . . . . . 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 ) )
113 uneq2 3584 . . . . . . . . . . . . . . . . . . . . . 22 |- ( p = ( f ` q ) -> ( s u. p ) = ( s u. ( f ` q ) ) )
114113eqeq2d 2463 . . . . . . . . . . . . . . . . . . . . 21 |- ( p = ( f ` q ) -> ( q = ( s u. p ) <-> q = ( s u. ( f ` q ) ) ) )
115114ac6sfi 7820 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
116115expcom 437 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
117112, 116syl 17 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
118 frn 5740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : d --> a -> ran f C_ a )
119118adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) -> ran f C_ a )
120119ad2antll 736 . . . . . . . . . . . . . . . . . . . . . . . 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 )
12135ad2antrr 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 ) ) ) ) ) -> s e. a )
122121snssd 4120 . . . . . . . . . . . . . . . . . . . . . . . 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 )
123120, 122unssd 3612 . . . . . . . . . . . . . . . . . . . . . . 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 )
124 simprl 765 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
125 simprrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
126 ffn 5733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f : d --> a -> f Fn d )
127125, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
128 dffn4 5804 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f Fn d <-> f : d -onto-> ran f )
129127, 128sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
130 fofi 7865 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. Fin /\ f : d -onto-> ran f ) -> ran f e. Fin )
131124, 129, 130syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . 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 )
132 snfi 7655 . . . . . . . . . . . . . . . . . . . . . . . 24 |- { s } e. Fin
133 unfi 7843 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran f e. Fin /\ { s } e. Fin ) -> ( ran f u. { s } ) e. Fin )
134131, 132, 133sylancl 669 . . . . . . . . . . . . . . . . . . . . . . 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 )
135 elfpw 7881 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ran f u. { s } ) e. ( ~P a i^i Fin ) <-> ( ( ran f u. { s } ) C_ a /\ ( ran f u. { s } ) e. Fin ) )
136123, 134, 135sylanbrc 671 . . . . . . . . . . . . . . . . . . . . . 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 ) )
137 simplrr 772 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
138 uniiun 4334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- U. d = U_ q e. d q
139 simprrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
140 iuneq2 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A. q e. d q = ( s u. ( f ` q ) ) -> U_ q e. d q = U_ q e. d ( s u. ( f ` q ) ) )
141139, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
142138, 141syl5eq 2499 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
143137, 142eqtrd 2487 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
144 ssun2 3600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- { s } C_ ( ran f u. { s } )
145 ssnid 3999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- s e. { s }
146144, 145sselii 3431 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- s e. ( ran f u. { s } )
147 elssuni 4230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( s e. ( ran f u. { s } ) -> s C_ U. ( ran f u. { s } ) )
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- s C_ U. ( ran f u. { s } )
149 fvssunirn 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f ` q ) C_ U. ran f
150 ssun1 3599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ran f C_ ( ran f u. { s } )
151150unissi 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- U. ran f C_ U. ( ran f u. { s } )
152149, 151sstri 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f ` q ) C_ U. ( ran f u. { s } )
153148, 152unssi 3611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
154153rgenw 2751 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- A. q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
155 iunss 4322 . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
156154, 155mpbir 213 . . . . . . . . . . . . . . . . . . . . . . . 24 |- U_ q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
157143, 156syl6eqss 3484 . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
15834ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
159120, 158sstrd 3444 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
16036ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
161160snssd 4120 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
162159, 161unssd 3612 . . . . . . . . . . . . . . . . . . . . . . . 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 )
163 uniss 4222 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ U. J )
164163, 2syl6sseqr 3481 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ X )
165162, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . 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 )
166157, 165eqssd 3451 . . . . . . . . . . . . . . . . . . . . . 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 } ) )
167 unieq 4209 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b = ( ran f u. { s } ) -> U. b = U. ( ran f u. { s } ) )
168167eqeq2d 2463 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( b = ( ran f u. { s } ) -> ( X = U. b <-> X = U. ( ran f u. { s } ) ) )
169168rspcev 3152 . . . . . . . . . . . . . . . . . . . . . 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 )
170136, 166, 169syl2anc 667 . . . . . . . . . . . . . . . . . . . . 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 )
171170expr 620 . . . . . . . . . . . . . . . . . . . 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 ) )
172171exlimdv 1781 . . . . . . . . . . . . . . . . . . 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 ) )
173172ex 436 . . . . . . . . . . . . . . . . . 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 ) ) )
174117, 173mpdd 41 . . . . . . . . . . . . . . . . 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 ) )
17592, 108, 1743syld 57 . . . . . . . . . . . . . . . 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 ) )
176175ex 436 . . . . . . . . . . . . . . 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 ) ) )
177176com23 81 . . . . . . . . . . . . . 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 ) ) )
178177rexlimdv 2879 . . . . . . . . . . . . 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 ) )
17978, 178syld 45 . . . . . . . . . . . 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 ) )
180179rexlimdvaa 2882 . . . . . . . . . . 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 ) ) )
18133, 180syld 45 . . . . . . . . . 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 ) ) )
182181exlimdv 1781 . . . . . . . . 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 ) ) )
18328, 182syl5bi 221 . . . . . . . 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 ) ) )
18427, 183pm2.61dne 2712 . . . . . . 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 ) )
18515, 184syl3an3 1304 . . . . . 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 ) )
1861853exp 1208 . . . . 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 ) ) ) )
187186com24 90 . . . 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 ) ) ) )
188187ralrimdv 2806 . . 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 ) ) )
1892iscmp 20415 . . . 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 ) ) )
190189baibr 916 . . 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 ) )
191188, 190sylibd 218 . 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 ) )
19214, 191impbid2 208 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 188   /\ wa 371   /\ w3a 986   = wceq 1446   E.wex 1665   e. wcel 1889   {cab 2439   =/= wne 2624   A.wral 2739   E.wrex 2740   {crab 2743   _Vcvv 3047   u. cun 3404   i^i cin 3405   C_ wss 3406   (/)c0 3733   ~Pcpw 3953   {csn 3970   U.cuni 4201   U_ciun 4281   |-> cmpt 4464   ran crn 4838   Fn wfn 5580   -->wf 5581   -onto->wfo 5583   ` cfv 5585   Fincfn 7574   Topctop 19929   Compccmp 20413   PtFincptfin 20530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-en 7575  df-dom 7576  df-fin 7578  df-top 19933  df-cmp 20414  df-ptfin 20533
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator