MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  comppfsc Structured version   Unicode version
Theorem comppfsc 20118
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 3936 . . . 4 |- ( c e. ~P J -> c C_ J )
2 comppfsc.1 . . . . . . 7 |- X = U. J
32cmpcov 19975 . . . . . 6 |- ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
4 elfpw 7737 . . . . . . . 8 |- ( d e. ( ~P c i^i Fin ) <-> ( d C_ c /\ d e. Fin ) )
5 finptfin 20104 . . . . . . . . . . 11 |- ( d e. Fin -> d e. PtFin )
65anim1i 566 . . . . . . . . . 10 |- ( ( d e. Fin /\ ( d C_ c /\ X = U. d ) ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
76anassrs 646 . . . . . . . . 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 470 . . . . . . 7 |- ( ( d e. ( ~P c i^i Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
109reximi2 2849 . . . . . 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 1193 . . . 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 2794 . 2 |- ( J e. Comp -> A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) )
15 elpwi 3936 . . . . . . 7 |- ( a e. ~P J -> a C_ J )
16 0elpw 4534 . . . . . . . . . . . 12 |- (/) e. ~P a
17 0fin 7663 . . . . . . . . . . . 12 |- (/) e. Fin
18 elin 3601 . . . . . . . . . . . 12 |- ( (/) e. ( ~P a i^i Fin ) <-> ( (/) e. ~P a /\ (/) e. Fin ) )
1916, 17, 18mpbir2an 918 . . . . . . . . . . 11 |- (/) e. ( ~P a i^i Fin )
20 unieq 4171 . . . . . . . . . . . . . 14 |- ( b = (/) -> U. b = U. (/) )
21 uni0 4190 . . . . . . . . . . . . . 14 |- U. (/) = (/)
2220, 21syl6eq 2439 . . . . . . . . . . . . 13 |- ( b = (/) -> U. b = (/) )
2322eqeq2d 2396 . . . . . . . . . . . 12 |- ( b = (/) -> ( X = U. b <-> X = (/) ) )
2423rspcev 3135 . . . . . . . . . . 11 |- ( ( (/) e. ( ~P a i^i Fin ) /\ X = (/) ) -> E. b e. ( ~P a i^i Fin ) X = U. b )
2519, 24mpan 668 . . . . . . . . . 10 |- ( X = (/) -> E. b e. ( ~P a i^i Fin ) X = U. b )
2625a1d 25 . . . . . . . . 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 3721 . . . . . . . . 9 |- ( X =/= (/) <-> E. x x e. X )
29 simp2 995 . . . . . . . . . . . . . 14 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> X = U. a )
3029eleq2d 2452 . . . . . . . . . . . . 13 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X <-> x e. U. a ) )
3130biimpd 207 . . . . . . . . . . . 12 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> x e. U. a ) )
32 eluni2 4167 . . . . . . . . . . . 12 |- ( x e. U. a <-> E. s e. a x e. s )
3331, 32syl6ib 226 . . . . . . . . . . 11 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> E. s e. a x e. s ) )
34 simpl3 999 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> a C_ J )
35 simprl 754 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. a )
3634, 35sseldd 3418 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
37 elssuni 4192 . . . . . . . . . . . . . . . . . . . . 21 |- ( s e. J -> s C_ U. J )
3837, 2syl6sseqr 3464 . . . . . . . . . . . . . . . . . . . 20 |- ( s e. J -> s C_ X )
3936, 38syl 16 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s C_ X )
4039ralrimivw 2797 . . . . . . . . . . . . . . . . . 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 4284 . . . . . . . . . . . . . . . . . 18 |- ( U_ p e. a s C_ X <-> A. p e. a s C_ X )
4240, 41sylibr 212 . . . . . . . . . . . . . . . . 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 3588 . . . . . . . . . . . . . . . . 17 |- ( U_ p e. a s C_ X <-> ( U_ p e. a s u. X ) = X )
4442, 43sylib 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 )
45 simpl2 998 . . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U. a )
46 uniiun 4296 . . . . . . . . . . . . . . . . . 18 |- U. a = U_ p e. a p
4745, 46syl6eq 2439 . . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U_ p e. a p )
4847uneq2d 3572 . . . . . . . . . . . . . . . 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 2425 . . . . . . . . . . . . . . 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 4327 . . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = ( U_ p e. a s u. U_ p e. a p )
51 vex 3037 . . . . . . . . . . . . . . . . . 18 |- s e. _V
52 vex 3037 . . . . . . . . . . . . . . . . . 18 |- p e. _V
5351, 52unex 6497 . . . . . . . . . . . . . . . . 17 |- ( s u. p ) e. _V
5453dfiun3 5170 . . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = U. ran ( p e. a |-> ( s u. p ) )
5550, 54eqtr3i 2413 . . . . . . . . . . . . . . 15 |- ( U_ p e. a s u. U_ p e. a p ) = U. ran ( p e. a |-> ( s u. p ) )
5649, 55syl6eq 2439 . . . . . . . . . . . . . 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 1033 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> J e. Top )
5836adantr 463 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> s e. J )
5934sselda 3417 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> p e. J )
60 unopn 19497 . . . . . . . . . . . . . . . . . . 19 |- ( ( J e. Top /\ s e. J /\ p e. J ) -> ( s u. p ) e. J )
6157, 58, 59, 60syl3anc 1226 . . . . . . . . . . . . . . . . . 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 2382 . . . . . . . . . . . . . . . . . 18 |- ( p e. a |-> ( s u. p ) ) = ( p e. a |-> ( s u. p ) )
6361, 62fmptd 5957 . . . . . . . . . . . . . . . . 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 5645 . . . . . . . . . . . . . . . . 17 |- ( ( p e. a |-> ( s u. p ) ) : a --> J -> ran ( p e. a |-> ( s u. p ) ) C_ J )
6563, 64syl 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 )
66 elpw2g 4528 . . . . . . . . . . . . . . . . . 18 |- ( J e. Top -> ( ran ( p e. a |-> ( s u. p ) ) e. ~P J <-> ran ( p e. a |-> ( s u. p ) ) C_ J ) )
67663ad2ant1 1015 . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . 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 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 )
70 unieq 4171 . . . . . . . . . . . . . . . . . 18 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> U. c = U. ran ( p e. a |-> ( s u. p ) ) )
7170eqeq2d 2396 . . . . . . . . . . . . . . . . 17 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( X = U. c <-> X = U. ran ( p e. a |-> ( s u. p ) ) ) )
72 sseq2 3439 . . . . . . . . . . . . . . . . . . 19 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( d C_ c <-> d C_ ran ( p e. a |-> ( s u. p ) ) ) )
7372anbi1d 702 . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . 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 318 . . . . . . . . . . . . . . . 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 3131 . . . . . . . . . . . . . . 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 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 ) ) ) )
7856, 77mpid 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 ) ) )
79 simprr 755 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. s )
80 ssel2 3412 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( a C_ J /\ s e. a ) -> s e. J )
81803ad2antl3 1158 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ s e. a ) -> s e. J )
8281adantrr 714 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
83 elunii 4168 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. s /\ s e. J ) -> x e. U. J )
8479, 82, 83syl2anc 659 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. U. J )
8584, 2syl6eleqr 2481 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. X )
8685adantr 463 . . . . . . . . . . . . . . . . . . 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 755 . . . . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . . . . 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 2382 . . . . . . . . . . . . . . . . . . . 20 |- U. d = U. d
9089ptfinfin 20105 . . . . . . . . . . . . . . . . . . 19 |- ( ( d e. PtFin /\ x e. U. d ) -> { z e. d | x e. z } e. Fin )
9190expcom 433 . . . . . . . . . . . . . . . . . 18 |- ( x e. U. d -> ( d e. PtFin -> { z e. d | x e. z } e. Fin ) )
9288, 91syl 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 ) )
93 simprl 754 . . . . . . . . . . . . . . . . . . . . 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 3585 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. s -> x e. ( s u. p ) )
9594ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. ( s u. p ) )
9695ralrimivw 2797 . . . . . . . . . . . . . . . . . . . . . . 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 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 |- A. p e. a ( s u. p ) e. _V
98 eleq2 2455 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = ( s u. p ) -> ( x e. z <-> x e. ( s u. p ) ) )
9962, 98ralrnmpt 5942 . . . . . . . . . . . . . . . . . . . . . . . 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 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 )
102101adantr 463 . . . . . . . . . . . . . . . . . . . . 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 3478 . . . . . . . . . . . . . . . . . . . . 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 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 )
105 rabid2 2960 . . . . . . . . . . . . . . . . . . . 20 |- ( d = { z e. d | x e. z } <-> A. z e. d x e. z )
106104, 105sylibr 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 } )
107106eleq1d 2451 . . . . . . . . . . . . . . . . . 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 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 ) )
10962rnmpt 5161 . . . . . . . . . . . . . . . . . . . . 21 |- ran ( p e. a |-> ( s u. p ) ) = { q | E. p e. a q = ( s u. p ) }
11093, 109syl6sseq 3463 . . . . . . . . . . . . . . . . . . . 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 3485 . . . . . . . . . . . . . . . . . . . 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 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 ) )
113 uneq2 3566 . . . . . . . . . . . . . . . . . . . . . 22 |- ( p = ( f ` q ) -> ( s u. p ) = ( s u. ( f ` q ) ) )
114113eqeq2d 2396 . . . . . . . . . . . . . . . . . . . . 21 |- ( p = ( f ` q ) -> ( q = ( s u. p ) <-> q = ( s u. ( f ` q ) ) ) )
115114ac6sfi 7679 . . . . . . . . . . . . . . . . . . . 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 433 . . . . . . . . . . . . . . . . . . 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 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 ) ) ) ) )
118 frn 5645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : d --> a -> ran f C_ a )
119118adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) -> ran f C_ a )
120119ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . . . . . . 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 4089 . . . . . . . . . . . . . . . . . . . . . . . 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 3594 . . . . . . . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . . . . . . . . . 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 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 )
126 ffn 5639 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f : d --> a -> f Fn d )
127125, 126syl 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 )
128 dffn4 5709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f Fn d <-> f : d -onto-> ran f )
129127, 128sylib 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 )
130 fofi 7721 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. Fin /\ f : d -onto-> ran f ) -> ran f e. Fin )
131124, 129, 130syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 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 7515 . . . . . . . . . . . . . . . . . . . . . . . 24 |- { s } e. Fin
133 unfi 7702 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran f e. Fin /\ { s } e. Fin ) -> ( ran f u. { s } ) e. Fin )
134131, 132, 133sylancl 660 . . . . . . . . . . . . . . . . . . . . . . 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 7737 . . . . . . . . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . . . . . . . . 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 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 )
138 uniiun 4296 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- U. d = U_ q e. d q
139 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 ) ) )
140 iuneq2 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) )
142138, 141syl5eq 2435 . . . . . . . . . . . . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . . . . . . . . . . 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 3582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- { s } C_ ( ran f u. { s } )
145 ssnid 3973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- s e. { s }
146144, 145sselii 3414 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- s e. ( ran f u. { s } )
147 elssuni 4192 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f ` q ) C_ U. ran f
150 ssun1 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ran f C_ ( ran f u. { s } )
151150unissi 4186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- U. ran f C_ U. ( ran f u. { s } )
152149, 151sstri 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f ` q ) C_ U. ( ran f u. { s } )
153148, 152unssi 3593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
154153rgenw 2743 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- A. q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
155 iunss 4284 . . . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . . . 24 |- U_ q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
157143, 156syl6eqss 3467 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> X C_ U. ( ran f u. { s } ) )
15834ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3427 . . . . . . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4089 . . . . . . . . . . . . . . . . . . . . . . . . 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 3594 . . . . . . . . . . . . . . . . . . . . . . . 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 4184 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ U. J )
164163, 2syl6sseqr 3464 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ X )
165162, 164syl 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 )
166157, 165eqssd 3434 . . . . . . . . . . . . . . . . . . . . . 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 4171 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b = ( ran f u. { s } ) -> U. b = U. ( ran f u. { s } ) )
168167eqeq2d 2396 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( b = ( ran f u. { s } ) -> ( X = U. b <-> X = U. ( ran f u. { s } ) ) )
169168rspcev 3135 . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . 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 613 . . . . . . . . . . . . . . . . . . . 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 1732 . . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . . . 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 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 ) )
17592, 108, 1743syld 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 ) )
176175ex 432 . . . . . . . . . . . . . . 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 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 ) ) )
178177rexlimdv 2872 . . . . . . . . . . . . 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 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 ) )
180179rexlimdvaa 2875 . . . . . . . . . . 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 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 ) ) )
182181exlimdv 1732 . . . . . . . . 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 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 ) ) )
18427, 183pm2.61dne 2699 . . . . . . 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 1261 . . . . . 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 1193 . . . . 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 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 ) ) ) )
188187ralrimdv 2798 . . 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 19974 . . . 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 902 . . 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 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 ) )
19214, 191impbid2 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 367   /\ w3a 971   = wceq 1399   E.wex 1620   e. wcel 1826   {cab 2367   =/= wne 2577   A.wral 2732   E.wrex 2733   {crab 2736   _Vcvv 3034   u. cun 3387   i^i cin 3388   C_ wss 3389   (/)c0 3711   ~Pcpw 3927   {csn 3944   U.cuni 4163   U_ciun 4243   |-> cmpt 4425   ran crn 4914   Fn wfn 5491   -->wf 5492   -onto->wfo 5494   ` cfv 5496   Fincfn 7435   Topctop 19479   Compccmp 19972   PtFincptfin 20089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-recs 6960  df-rdg 6994  df-1o 7048  df-oadd 7052  df-er 7229  df-en 7436  df-dom 7437  df-fin 7439  df-top 19484  df-cmp 19973  df-ptfin 20092
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator