Metamath Proof Explorer

Theorem comppfsc

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)

Ref Expression
Hypothesis comppfsc.1 
|- X = U. J
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 comppfsc.1 
 |-  X = U. J
2 elpwi 
 |-  ( c e. ~P J -> c C_ J )
3 1 cmpcov 
 |-  ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
4 elfpw 
 |-  ( d e. ( ~P c i^i Fin ) <-> ( d C_ c /\ d e. Fin ) )
5 finptfin 
 |-  ( d e. Fin -> d e. PtFin )
6 5 anim1i 
 |-  ( ( d e. Fin /\ ( d C_ c /\ X = U. d ) ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
7 6 anassrs 
 |-  ( ( ( d e. Fin /\ d C_ c ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
8 7 ancom1s 
 |-  ( ( ( d C_ c /\ d e. Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
9 4 8 sylanb 
 |-  ( ( d e. ( ~P c i^i Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
10 9 reximi2 
 |-  ( E. d e. ( ~P c i^i Fin ) X = U. d -> E. d e. PtFin ( d C_ c /\ X = U. d ) )
11 3 10 syl 
 |-  ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. PtFin ( d C_ c /\ X = U. d ) )
12 11 3exp 
 |-  ( J e. Comp -> ( c C_ J -> ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )
13 2 12 syl5 
 |-  ( J e. Comp -> ( c e. ~P J -> ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )
14 13 ralrimiv 
 |-  ( J e. Comp -> A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) )
15 elpwi 
 |-  ( a e. ~P J -> a C_ J )
16 0elpw 
 |-  (/) e. ~P a
17 0fi 
 |-  (/) e. Fin
18 16 17 elini 
 |-  (/) e. ( ~P a i^i Fin )
19 unieq 
 |-  ( b = (/) -> U. b = U. (/) )
20 uni0 
 |-  U. (/) = (/)
21 19 20 eqtrdi 
 |-  ( b = (/) -> U. b = (/) )
22 21 rspceeqv 
 |-  ( ( (/) e. ( ~P a i^i Fin ) /\ X = (/) ) -> E. b e. ( ~P a i^i Fin ) X = U. b )
23 18 22 mpan 
 |-  ( X = (/) -> E. b e. ( ~P a i^i Fin ) X = U. b )
24 23 a1i13 
 |-  ( ( 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 ) ) )
25 n0 
 |-  ( X =/= (/) <-> E. x x e. X )
26 simp2 
 |-  ( ( J e. Top /\ X = U. a /\ a C_ J ) -> X = U. a )
27 26 eleq2d 
 |-  ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X <-> x e. U. a ) )
28 27 biimpd 
 |-  ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> x e. U. a ) )
29 eluni2 
 |-  ( x e. U. a <-> E. s e. a x e. s )
30 28 29 imbitrdi 
 |-  ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> E. s e. a x e. s ) )
31 simpl3 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> a C_ J )
32 simprl 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. a )
33 31 32 sseldd 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
34 elssuni 
 |-  ( s e. J -> s C_ U. J )
35 34 1 sseqtrrdi 
 |-  ( s e. J -> s C_ X )
36 33 35 syl 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s C_ X )
37 36 ralrimivw 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> A. p e. a s C_ X )
38 iunss 
 |-  ( U_ p e. a s C_ X <-> A. p e. a s C_ X )
39 37 38 sylibr 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> U_ p e. a s C_ X )
40 ssequn1 
 |-  ( U_ p e. a s C_ X <-> ( U_ p e. a s u. X ) = X )
41 39 40 sylib 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( U_ p e. a s u. X ) = X )
42 simpl2 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U. a )
43 uniiun 
 |-  U. a = U_ p e. a p
44 42 43 eqtrdi 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U_ p e. a p )
45 44 uneq2d 
 |-  ( ( ( 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 ) )
46 41 45 eqtr3d 
 |-  ( ( ( 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 ) )
47 iunun 
 |-  U_ p e. a ( s u. p ) = ( U_ p e. a s u. U_ p e. a p )
48 vex 
 |-  s e. _V
49 vex 
 |-  p e. _V
50 48 49 unex 
 |-  ( s u. p ) e. _V
51 50 dfiun3 
 |-  U_ p e. a ( s u. p ) = U. ran ( p e. a |-> ( s u. p ) )
52 47 51 eqtr3i 
 |-  ( U_ p e. a s u. U_ p e. a p ) = U. ran ( p e. a |-> ( s u. p ) )
53 46 52 eqtrdi 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U. ran ( p e. a |-> ( s u. p ) ) )
54 simpll1 
 |-  ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> J e. Top )
55 33 adantr 
 |-  ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> s e. J )
56 31 sselda 
 |-  ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> p e. J )
57 unopn 
 |-  ( ( J e. Top /\ s e. J /\ p e. J ) -> ( s u. p ) e. J )
58 54 55 56 57 syl3anc 
 |-  ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> ( s u. p ) e. J )
59 58 fmpttd 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( p e. a |-> ( s u. p ) ) : a --> J )
60 59 frnd 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ran ( p e. a |-> ( s u. p ) ) C_ J )
61 elpw2g 
 |-  ( J e. Top -> ( ran ( p e. a |-> ( s u. p ) ) e. ~P J <-> ran ( p e. a |-> ( s u. p ) ) C_ J ) )
62 61 3ad2ant1 
 |-  ( ( 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 ) )
63 62 adantr 
 |-  ( ( ( 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 ) )
64 60 63 mpbird 
 |-  ( ( ( 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 )
65 unieq 
 |-  ( c = ran ( p e. a |-> ( s u. p ) ) -> U. c = U. ran ( p e. a |-> ( s u. p ) ) )
66 65 eqeq2d 
 |-  ( c = ran ( p e. a |-> ( s u. p ) ) -> ( X = U. c <-> X = U. ran ( p e. a |-> ( s u. p ) ) ) )
67 sseq2 
 |-  ( c = ran ( p e. a |-> ( s u. p ) ) -> ( d C_ c <-> d C_ ran ( p e. a |-> ( s u. p ) ) ) )
68 67 anbi1d 
 |-  ( 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 ) ) )
69 68 rexbidv 
 |-  ( 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 ) ) )
70 66 69 imbi12d 
 |-  ( 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 ) ) ) )
71 70 rspcv 
 |-  ( 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 ) ) ) )
72 64 71 syl 
 |-  ( ( ( 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 ) ) ) )
73 53 72 mpid 
 |-  ( ( ( 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 ) ) )
74 simprr 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. s )
75 ssel2 
 |-  ( ( a C_ J /\ s e. a ) -> s e. J )
76 75 3ad2antl3 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ s e. a ) -> s e. J )
77 76 adantrr 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
78 elunii 
 |-  ( ( x e. s /\ s e. J ) -> x e. U. J )
79 74 77 78 syl2anc 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. U. J )
80 79 1 eleqtrrdi 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. X )
81 80 adantr 
 |-  ( ( ( ( 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 )
82 simprr 
 |-  ( ( ( ( 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 )
83 81 82 eleqtrd 
 |-  ( ( ( ( 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 )
84 eqid 
 |-  U. d = U. d
85 84 ptfinfin 
 |-  ( ( d e. PtFin /\ x e. U. d ) -> { z e. d | x e. z } e. Fin )
86 85 expcom 
 |-  ( x e. U. d -> ( d e. PtFin -> { z e. d | x e. z } e. Fin ) )
87 83 86 syl 
 |-  ( ( ( ( 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 ) )
88 simprl 
 |-  ( ( ( ( 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 ) ) )
89 elun1 
 |-  ( x e. s -> x e. ( s u. p ) )
90 89 ad2antll 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. ( s u. p ) )
91 90 ralrimivw 
 |-  ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> A. p e. a x e. ( s u. p ) )
92 50 rgenw 
 |-  A. p e. a ( s u. p ) e. _V
93 eqid 
 |-  ( p e. a |-> ( s u. p ) ) = ( p e. a |-> ( s u. p ) )
94 eleq2 
 |-  ( z = ( s u. p ) -> ( x e. z <-> x e. ( s u. p ) ) )
95 93 94 ralrnmptw 
 |-  ( 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 ) ) )
96 92 95 ax-mp 
 |-  ( A. z e. ran ( p e. a |-> ( s u. p ) ) x e. z <-> A. p e. a x e. ( s u. p ) )
97 91 96 sylibr 
 |-  ( ( ( 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 )
98 97 adantr 
 |-  ( ( ( ( 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 )
99 ssralv 
 |-  ( 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 ) )
100 88 98 99 sylc 
 |-  ( ( ( ( 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 )
101 rabid2 
 |-  ( d = { z e. d | x e. z } <-> A. z e. d x e. z )
102 100 101 sylibr 
 |-  ( ( ( ( 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 } )
103 102 eleq1d 
 |-  ( ( ( ( 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 ) )
104 103 biimprd 
 |-  ( ( ( ( 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 ) )
105 93 rnmpt 
 |-  ran ( p e. a |-> ( s u. p ) ) = { q | E. p e. a q = ( s u. p ) }
106 88 105 sseqtrdi 
 |-  ( ( ( ( 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 ) } )
107 ssabral 
 |-  ( d C_ { q | E. p e. a q = ( s u. p ) } <-> A. q e. d E. p e. a q = ( s u. p ) )
108 106 107 sylib 
 |-  ( ( ( ( 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 ) )
109 uneq2 
 |-  ( p = ( f ` q ) -> ( s u. p ) = ( s u. ( f ` q ) ) )
110 109 eqeq2d 
 |-  ( p = ( f ` q ) -> ( q = ( s u. p ) <-> q = ( s u. ( f ` q ) ) ) )
111 110 ac6sfi 
 |-  ( ( 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 ) ) ) )
112 111 expcom 
 |-  ( 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 ) ) ) ) )
113 108 112 syl 
 |-  ( ( ( ( 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 ) ) ) ) )
114 frn 
 |-  ( f : d --> a -> ran f C_ a )
115 114 adantr 
 |-  ( ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) -> ran f C_ a )
116 115 ad2antll 
 |-  ( ( ( ( ( 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 )
117 32 ad2antrr 
 |-  ( ( ( ( ( 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 )
118 117 snssd 
 |-  ( ( ( ( ( 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 )
119 116 118 unssd 
 |-  ( ( ( ( ( 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 )
120 simprl 
 |-  ( ( ( ( ( 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 )
121 simprrl 
 |-  ( ( ( ( ( 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 )
122 121 ffnd 
 |-  ( ( ( ( ( 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 )
123 dffn4 
 |-  ( f Fn d <-> f : d -onto-> ran f )
124 122 123 sylib 
 |-  ( ( ( ( ( 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 )
125 fofi 
 |-  ( ( d e. Fin /\ f : d -onto-> ran f ) -> ran f e. Fin )
126 120 124 125 syl2anc 
 |-  ( ( ( ( ( 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 )
127 snfi 
 |-  { s } e. Fin
128 unfi 
 |-  ( ( ran f e. Fin /\ { s } e. Fin ) -> ( ran f u. { s } ) e. Fin )
129 126 127 128 sylancl 
 |-  ( ( ( ( ( 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 )
130 elfpw 
 |-  ( ( ran f u. { s } ) e. ( ~P a i^i Fin ) <-> ( ( ran f u. { s } ) C_ a /\ ( ran f u. { s } ) e. Fin ) )
131 119 129 130 sylanbrc 
 |-  ( ( ( ( ( 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 ) )
132 simplrr 
 |-  ( ( ( ( ( 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 )
133 uniiun 
 |-  U. d = U_ q e. d q
134 simprrr 
 |-  ( ( ( ( ( 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 ) ) )
135 iuneq2 
 |-  ( A. q e. d q = ( s u. ( f ` q ) ) -> U_ q e. d q = U_ q e. d ( s u. ( f ` q ) ) )
136 134 135 syl 
 |-  ( ( ( ( ( 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 ) ) )
137 133 136 eqtrid 
 |-  ( ( ( ( ( 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 ) ) )
138 132 137 eqtrd 
 |-  ( ( ( ( ( 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 ) ) )
139 ssun2 
 |-  { s } C_ ( ran f u. { s } )
140 vsnid 
 |-  s e. { s }
141 139 140 sselii 
 |-  s e. ( ran f u. { s } )
142 elssuni 
 |-  ( s e. ( ran f u. { s } ) -> s C_ U. ( ran f u. { s } ) )
143 141 142 ax-mp 
 |-  s C_ U. ( ran f u. { s } )
144 fvssunirn 
 |-  ( f ` q ) C_ U. ran f
145 ssun1 
 |-  ran f C_ ( ran f u. { s } )
146 145 unissi 
 |-  U. ran f C_ U. ( ran f u. { s } )
147 144 146 sstri 
 |-  ( f ` q ) C_ U. ( ran f u. { s } )
148 143 147 unssi 
 |-  ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
149 148 rgenw 
 |-  A. q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
150 iunss 
 |-  ( 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 } ) )
151 149 150 mpbir 
 |-  U_ q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
152 138 151 eqsstrdi 
 |-  ( ( ( ( ( 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 } ) )
153 31 ad2antrr 
 |-  ( ( ( ( ( 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 )
154 116 153 sstrd 
 |-  ( ( ( ( ( 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 )
155 33 ad2antrr 
 |-  ( ( ( ( ( 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 )
156 155 snssd 
 |-  ( ( ( ( ( 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 )
157 154 156 unssd 
 |-  ( ( ( ( ( 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 )
158 uniss 
 |-  ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ U. J )
159 158 1 sseqtrrdi 
 |-  ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ X )
160 157 159 syl 
 |-  ( ( ( ( ( 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 )
161 152 160 eqssd 
 |-  ( ( ( ( ( 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 } ) )
162 unieq 
 |-  ( b = ( ran f u. { s } ) -> U. b = U. ( ran f u. { s } ) )
163 162 rspceeqv 
 |-  ( ( ( 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 )
164 131 161 163 syl2anc 
 |-  ( ( ( ( ( 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 )
165 164 expr 
 |-  ( ( ( ( ( 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 ) )
166 165 exlimdv 
 |-  ( ( ( ( ( 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 ) )
167 166 ex 
 |-  ( ( ( ( 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 ) ) )
168 113 167 mpdd 
 |-  ( ( ( ( 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 ) )
169 87 104 168 3syld 
 |-  ( ( ( ( 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 ) )
170 169 ex 
 |-  ( ( ( 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 ) ) )
171 170 com23 
 |-  ( ( ( 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 ) ) )
172 171 rexlimdv 
 |-  ( ( ( 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 ) )
173 73 172 syld 
 |-  ( ( ( 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 ) )
174 173 rexlimdvaa 
 |-  ( ( 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 ) ) )
175 30 174 syld 
 |-  ( ( 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 ) ) )
176 175 exlimdv 
 |-  ( ( 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 ) ) )
177 25 176 biimtrid 
 |-  ( ( 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 ) ) )
178 24 177 pm2.61dne 
 |-  ( ( 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 ) )
179 15 178 syl3an3 
 |-  ( ( 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 ) )
180 179 3exp 
 |-  ( 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 ) ) ) )
181 180 com24 
 |-  ( 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 ) ) ) )
182 181 ralrimdv 
 |-  ( 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 ) ) )
183 1 iscmp 
 |-  ( 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 ) ) )
184 183 baibr 
 |-  ( 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 ) )
185 182 184 sylibd 
 |-  ( J e. Top -> ( A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) -> J e. Comp ) )
186 14 185 impbid2 
 |-  ( J e. Top -> ( J e. Comp <-> A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )