Theorem comppfsc 28423

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.

Step	Hyp	Ref	Expression
1		elpwi 3857	. . . 4 |- ( c e. ~P J -> c C_ J )
2		comppfsc.1	. . . . . . 7 |- X = U. J
3	2	cmpcov 18834	. . . . . 6 |- ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
4		elfpw 7601	. . . . . . . 8 |- ( d e. ( ~P c i^i Fin ) <-> ( d C_ c /\ d e. Fin ) )
5		finptfin 28413	. . . . . . . . . . 11 |- ( d e. Fin -> d e. PtFin )
6	5	anim1i 563	. . . . . . . . . 10 |- ( ( d e. Fin /\ ( d C_ c /\ X = U. d ) ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
7	6	anassrs 641	. . . . . . . . 9 |- ( ( ( d e. Fin /\ d C_ c ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
8	7	ancom1s 796	. . . . . . . 8 |- ( ( ( d C_ c /\ d e. Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
9	4, 8	sylanb 469	. . . . . . 7 |- ( ( d e. ( ~P c i^i Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
10	9	reximi2 2812	. . . . . 6 |- ( 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 16	. . . . 5 |- ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. PtFin ( d C_ c /\ X = U. d ) )
12	11	3exp 1179	. . . 4 |- ( J e. Comp -> ( c C_ J -> ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )
13	1, 12	syl5 32	. . 3 |- ( J e. Comp -> ( c e. ~P J -> ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )
14	13	ralrimiv 2788	. 2 |- ( J e. Comp -> A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) )
15		elpwi 3857	. . . . . . 7 |- ( a e. ~P J -> a C_ J )
16		0elpw 4449	. . . . . . . . . . 11 |- (/) e. ~P a
17		0fin 7528	. . . . . . . . . . 11 |- (/) e. Fin
18		elin 3527	. . . . . . . . . . 11 |- ( (/) e. ( ~P a i^i Fin ) <-> ( (/) e. ~P a /\ (/) e. Fin ) )
19	16, 17, 18	mpbir2an 904	. . . . . . . . . 10 |- (/) e. ( ~P a i^i Fin )
20		unieq 4087	. . . . . . . . . . . . 13 |- ( b = (/) -> U. b = U. (/) )
21		uni0 4106	. . . . . . . . . . . . 13 |- U. (/) = (/)
22	20, 21	syl6eq 2481	. . . . . . . . . . . 12 |- ( b = (/) -> U. b = (/) )
23	22	eqeq2d 2444	. . . . . . . . . . 11 |- ( b = (/) -> ( X = U. b <-> X = (/) ) )
24	23	rspcev 3062	. . . . . . . . . 10 |- ( ( (/) e. ( ~P a i^i Fin ) /\ X = (/) ) -> E. b e. ( ~P a i^i Fin ) X = U. b )
25	19, 24	mpan 663	. . . . . . . . 9 |- ( X = (/) -> E. b e. ( ~P a i^i Fin ) X = U. b )
26	25	a1i13 28334	. . . . . . . 8 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( X = (/) -> ( A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )
27		n0 3634	. . . . . . . . 9 |- ( X =/= (/) <-> E. x x e. X )
28		simp2 982	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> X = U. a )
29	28	eleq2d 2500	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X <-> x e. U. a ) )
30	29	biimpd 207	. . . . . . . . . . . 12 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> x e. U. a ) )
31		eluni2 4083	. . . . . . . . . . . 12 |- ( x e. U. a <-> E. s e. a x e. s )
32	30, 31	syl6ib 226	. . . . . . . . . . 11 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> ( x e. X -> E. s e. a x e. s ) )
33		simpl3 986	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> a C_ J )
34		simprl 748	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. a )
35	33, 34	sseldd 3345	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
36		elssuni 4109	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. J -> s C_ U. J )
37	36, 2	syl6sseqr 3391	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. J -> s C_ X )
38	35, 37	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s C_ X )
39	38	ralrimivw 2790	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> A. p e. a s C_ X )
40		iunss 4199	. . . . . . . . . . . . . . . . . 18 |- ( U_ p e. a s C_ X <-> A. p e. a s C_ X )
41	39, 40	sylibr 212	. . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> U_ p e. a s C_ X )
42		ssequn1 3514	. . . . . . . . . . . . . . . . 17 |- ( U_ p e. a s C_ X <-> ( U_ p e. a s u. X ) = X )
43	41, 42	sylib 196	. . . . . . . . . . . . . . . 16 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( U_ p e. a s u. X ) = X )
44		simpl2 985	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U. a )
45		uniiun 4211	. . . . . . . . . . . . . . . . . 18 |- U. a = U_ p e. a p
46	44, 45	syl6eq 2481	. . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U_ p e. a p )
47	46	uneq2d 3498	. . . . . . . . . . . . . . . 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 ) )
48	43, 47	eqtr3d 2467	. . . . . . . . . . . . . . 15 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = ( U_ p e. a s u. U_ p e. a p ) )
49		iunun 4239	. . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = ( U_ p e. a s u. U_ p e. a p )
50		vex 2965	. . . . . . . . . . . . . . . . . 18 |- s e. _V
51		vex 2965	. . . . . . . . . . . . . . . . . 18 |- p e. _V
52	50, 51	unex 6367	. . . . . . . . . . . . . . . . 17 |- ( s u. p ) e. _V
53	52	dfiun3 5081	. . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = U. ran ( p e. a |-> ( s u. p ) )
54	49, 53	eqtr3i 2455	. . . . . . . . . . . . . . 15 |- ( U_ p e. a s u. U_ p e. a p ) = U. ran ( p e. a |-> ( s u. p ) )
55	48, 54	syl6eq 2481	. . . . . . . . . . . . . 14 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U. ran ( p e. a |-> ( s u. p ) ) )
56		simpll1 1020	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> J e. Top )
57	35	adantr 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> s e. J )
58	33	sselda 3344	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> p e. J )
59		unopn 18358	. . . . . . . . . . . . . . . . . . 19 |- ( ( J e. Top /\ s e. J /\ p e. J ) -> ( s u. p ) e. J )
60	56, 57, 58, 59	syl3anc 1211	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> ( s u. p ) e. J )
61		eqid 2433	. . . . . . . . . . . . . . . . . 18 |- ( p e. a |-> ( s u. p ) ) = ( p e. a |-> ( s u. p ) )
62	60, 61	fmptd 5855	. . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( p e. a |-> ( s u. p ) ) : a --> J )
63		frn 5553	. . . . . . . . . . . . . . . . 17 |- ( ( p e. a |-> ( s u. p ) ) : a --> J -> ran ( p e. a |-> ( s u. p ) ) C_ J )
64	62, 63	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ran ( p e. a |-> ( s u. p ) ) C_ J )
65		elpw2g 4443	. . . . . . . . . . . . . . . . . 18 |- ( J e. Top -> ( ran ( p e. a |-> ( s u. p ) ) e. ~P J <-> ran ( p e. a |-> ( s u. p ) ) C_ J ) )
66	65	3ad2ant1 1002	. . . . . . . . . . . . . . . . 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 ) )
67	66	adantr 462	. . . . . . . . . . . . . . . 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 ) )
68	64, 67	mpbird 232	. . . . . . . . . . . . . . 15 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ran ( p e. a |-> ( s u. p ) ) e. ~P J )
69		unieq 4087	. . . . . . . . . . . . . . . . . 18 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> U. c = U. ran ( p e. a |-> ( s u. p ) ) )
70	69	eqeq2d 2444	. . . . . . . . . . . . . . . . 17 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( X = U. c <-> X = U. ran ( p e. a |-> ( s u. p ) ) ) )
71		sseq2 3366	. . . . . . . . . . . . . . . . . . 19 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( d C_ c <-> d C_ ran ( p e. a |-> ( s u. p ) ) ) )
72	71	anbi1d 697	. . . . . . . . . . . . . . . . . 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 ) ) )
73	72	rexbidv 2726	. . . . . . . . . . . . . . . . 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 ) ) )
74	70, 73	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) <-> ( X = U. ran ( p e. a |-> ( s u. p ) ) -> E. d e. PtFin ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) ) )
75	74	rspcv 3058	. . . . . . . . . . . . . . 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 ) ) ) )
76	68, 75	syl 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 ) ) ) )
77	55, 76	mpid 41	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) -> E. d e. PtFin ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) )
78		simprr 749	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. s )
79		ssel2 3339	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( a C_ J /\ s e. a ) -> s e. J )
80	79	3ad2antl3 1145	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ s e. a ) -> s e. J )
81	80	adantrr 709	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
82		elunii 4084	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. s /\ s e. J ) -> x e. U. J )
83	78, 81, 82	syl2anc 654	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. U. J )
84	83, 2	syl6eleqr 2524	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. X )
85	84	adantr 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> x e. X )
86		simprr 749	. . . . . . . . . . . . . . . . . . 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 )
87	85, 86	eleqtrd 2509	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> x e. U. d )
88		eqid 2433	. . . . . . . . . . . . . . . . . . . 20 |- U. d = U. d
89	88	ptfinfin 28414	. . . . . . . . . . . . . . . . . . 19 |- ( ( d e. PtFin /\ x e. U. d ) -> { z e. d | x e. z } e. Fin )
90	89	expcom 435	. . . . . . . . . . . . . . . . . 18 |- ( x e. U. d -> ( d e. PtFin -> { z e. d | x e. z } e. Fin ) )
91	87, 90	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> ( d e. PtFin -> { z e. d | x e. z } e. Fin ) )
92		simprl 748	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> d C_ ran ( p e. a |-> ( s u. p ) ) )
93		elun1 3511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. s -> x e. ( s u. p ) )
94	93	ad2antll 721	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. ( s u. p ) )
95	94	ralrimivw 2790	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
96	52	rgenw 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 |- A. p e. a ( s u. p ) e. _V
97		eleq2 2494	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = ( s u. p ) -> ( x e. z <-> x e. ( s u. p ) ) )
98	61, 97	ralrnmpt 5840	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
99	96, 98	ax-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 ) )
100	95, 99	sylibr 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 )
101	100	adantr 462	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> A. z e. ran ( p e. a |-> ( s u. p ) ) x e. z )
102		ssralv 3404	. . . . . . . . . . . . . . . . . . . . 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 ) )
103	92, 101, 102	sylc 60	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> A. z e. d x e. z )
104		rabid2 2888	. . . . . . . . . . . . . . . . . . . 20 |- ( d = { z e. d | x e. z } <-> A. z e. d x e. z )
105	103, 104	sylibr 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 } )
106	105	eleq1d 2499	. . . . . . . . . . . . . . . . . 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 ) )
107	106	biimprd 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 ) )
108	61	rnmpt 5072	. . . . . . . . . . . . . . . . . . . . 21 |- ran ( p e. a |-> ( s u. p ) ) = { q | E. p e. a q = ( s u. p ) }
109	92, 108	syl6sseq 3390	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> d C_ { q | E. p e. a q = ( s u. p ) } )
110		ssabral 3411	. . . . . . . . . . . . . . . . . . . 20 |- ( d C_ { q | E. p e. a q = ( s u. p ) } <-> A. q e. d E. p e. a q = ( s u. p ) )
111	109, 110	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> A. q e. d E. p e. a q = ( s u. p ) )
112		uneq2 3492	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = ( f ` q ) -> ( s u. p ) = ( s u. ( f ` q ) ) )
113	112	eqeq2d 2444	. . . . . . . . . . . . . . . . . . . . 21 |- ( p = ( f ` q ) -> ( q = ( s u. p ) <-> q = ( s u. ( f ` q ) ) ) )
114	113	ac6sfi 7544	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
115	114	expcom 435	. . . . . . . . . . . . . . . . . . 19 |- ( A. q e. d E. p e. a q = ( s u. p ) -> ( d e. Fin -> E. f ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) )
116	111, 115	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> ( d e. Fin -> E. f ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) )
117		frn 5553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : d --> a -> ran f C_ a )
118	117	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) -> ran f C_ a )
119	118	ad2antll 721	. . . . . . . . . . . . . . . . . . . . . . . 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 )
120	34	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
121	120	snssd 4006	. . . . . . . . . . . . . . . . . . . . . . . 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 )
122	119, 121	unssd 3520	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> ( ran f u. { s } ) C_ a )
123		simprl 748	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> d e. Fin )
124		simprrl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> f : d --> a )
125		ffn 5547	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f : d --> a -> f Fn d )
126	124, 125	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> f Fn d )
127		dffn4 5614	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f Fn d <-> f : d -onto-> ran f )
128	126, 127	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> f : d -onto-> ran f )
129		fofi 7585	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. Fin /\ f : d -onto-> ran f ) -> ran f e. Fin )
130	123, 128, 129	syl2anc 654	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> ran f e. Fin )
131		snfi 7378	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { s } e. Fin
132		unfi 7567	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran f e. Fin /\ { s } e. Fin ) -> ( ran f u. { s } ) e. Fin )
133	130, 131, 132	sylancl 655	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> ( ran f u. { s } ) e. Fin )
134		elfpw 7601	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ran f u. { s } ) e. ( ~P a i^i Fin ) <-> ( ( ran f u. { s } ) C_ a /\ ( ran f u. { s } ) e. Fin ) )
135	122, 133, 134	sylanbrc 657	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> ( ran f u. { s } ) e. ( ~P a i^i Fin ) )
136		simplrr 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> X = U. d )
137		uniiun 4211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- U. d = U_ q e. d q
138		simprrr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> A. q e. d q = ( s u. ( f ` q ) ) )
139		iuneq2 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A. q e. d q = ( s u. ( f ` q ) ) -> U_ q e. d q = U_ q e. d ( s u. ( f ` q ) ) )
140	138, 139	syl 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 ) ) )
141	137, 140	syl5eq 2477	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
142	136, 141	eqtrd 2465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> X = U_ q e. d ( s u. ( f ` q ) ) )
143		ssun2 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- { s } C_ ( ran f u. { s } )
144		ssnid 3894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- s e. { s }
145	143, 144	sselii 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- s e. ( ran f u. { s } )
146		elssuni 4109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( s e. ( ran f u. { s } ) -> s C_ U. ( ran f u. { s } ) )
147	145, 146	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- s C_ U. ( ran f u. { s } )
148		fvssunirn 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f ` q ) C_ U. ran f
149		ssun1 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ran f C_ ( ran f u. { s } )
150	149	unissi 4102	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- U. ran f C_ U. ( ran f u. { s } )
151	148, 150	sstri 3353	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f ` q ) C_ U. ( ran f u. { s } )
152	147, 151	unssi 3519	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
153	152	rgenw 2773	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- A. q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
154		iunss 4199	. . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
155	153, 154	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . 24 |- U_ q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
156	142, 155	syl6eqss 3394	. . . . . . . . . . . . . . . . . . . . . . 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 } ) )
157	33	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . 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 )
158	119, 157	sstrd 3354	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
159	35	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . 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 )
160	159	snssd 4006	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
161	158, 160	unssd 3520	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> ( ran f u. { s } ) C_ J )
162		uniss 4100	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ U. J )
163	162, 2	syl6sseqr 3391	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ X )
164	161, 163	syl 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 )
165	156, 164	eqssd 3361	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) /\ ( d e. Fin /\ ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) ) ) -> X = U. ( ran f u. { s } ) )
166		unieq 4087	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b = ( ran f u. { s } ) -> U. b = U. ( ran f u. { s } ) )
167	166	eqeq2d 2444	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( b = ( ran f u. { s } ) -> ( X = U. b <-> X = U. ( ran f u. { s } ) ) )
168	167	rspcev 3062	. . . . . . . . . . . . . . . . . . . . . 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 )
169	135, 165, 168	syl2anc 654	. . . . . . . . . . . . . . . . . . . . 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 )
170	169	expr 610	. . . . . . . . . . . . . . . . . . . 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 ) )
171	170	exlimdv 1689	. . . . . . . . . . . . . . . . . . 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 ) )
172	171	ex 434	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) ) -> ( d e. Fin -> ( E. f ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )
173	116, 172	mpdd 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 ) )
174	91, 107, 173	3syld 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 ) )
175	174	ex 434	. . . . . . . . . . . . . . 15 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> ( ( d C_ ran ( p e. a |-> ( s u. p ) ) /\ X = U. d ) -> ( d e. PtFin -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )
176	175	com23 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 ) ) )
177	176	rexlimdv 2830	. . . . . . . . . . . . 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 ) )
178	77, 177	syld 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 ) )
179	178	rexlimdvaa 2832	. . . . . . . . . . 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 ) ) )
180	32, 179	syld 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 ) ) )
181	180	exlimdv 1689	. . . . . . . . 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 ) ) )
182	27, 181	syl5bi 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 ) ) )
183	26, 182	pm2.61dne 2678	. . . . . . 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 ) )
184	15, 183	syl3an3 1246	. . . . . 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 ) )
185	184	3exp 1179	. . . . 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 ) ) ) )
186	185	com24 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 ) ) ) )
187	186	ralrimdv 2795	. . 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 ) ) )
188	2	iscmp 18833	. . . 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 ) ) )
189	188	baibr 890	. . 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 ) )
190	187, 189	sylibd 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 ) )
191	14, 190	impbid2 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 ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 958   = wceq 1362   E.wex 1589   e. wcel 1755   {cab 2419   =/= wne 2596   A.wral 2705   E.wrex 2706   {crab 2709   _Vcvv 2962   u. cun 3314   i^i cin 3315   C_ wss 3316   (/)c0 3625   ~Pcpw 3848   {csn 3865   U.cuni 4079   U_ciun 4159   e. cmpt 4338   ran crn 4828   Fn wfn 5401   -->wf 5402   -onto->wfo 5404   ` cfv 5406   Fincfn 7298   Topctop 18340   Compccmp 18831   PtFincptfin 28377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-en 7299  df-dom 7300  df-fin 7302  df-top 18345  df-cmp 18832  df-ptfin 28381

This theorem is referenced by: (None)