Theorem comppfsc 28726

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 3976	. . . 4 |- ( c e. ~P J -> c C_ J )
2		comppfsc.1	. . . . . . 7 |- X = U. J
3	2	cmpcov 19123	. . . . . 6 |- ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
4		elfpw 7723	. . . . . . . 8 |- ( d e. ( ~P c i^i Fin ) <-> ( d C_ c /\ d e. Fin ) )
5		finptfin 28716	. . . . . . . . . . 11 |- ( d e. Fin -> d e. PtFin )
6	5	anim1i 568	. . . . . . . . . 10 |- ( ( d e. Fin /\ ( d C_ c /\ X = U. d ) ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
7	6	anassrs 648	. . . . . . . . 9 |- ( ( ( d e. Fin /\ d C_ c ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
8	7	ancom1s 803	. . . . . . . 8 |- ( ( ( d C_ c /\ d e. Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
9	4, 8	sylanb 472	. . . . . . 7 |- ( ( d e. ( ~P c i^i Fin ) /\ X = U. d ) -> ( d e. PtFin /\ ( d C_ c /\ X = U. d ) ) )
10	9	reximi2 2926	. . . . . 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 1187	. . . 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 2827	. 2 |- ( J e. Comp -> A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) )
15		elpwi 3976	. . . . . . 7 |- ( a e. ~P J -> a C_ J )
16		0elpw 4568	. . . . . . . . . . 11 |- (/) e. ~P a
17		0fin 7650	. . . . . . . . . . 11 |- (/) e. Fin
18		elin 3646	. . . . . . . . . . 11 |- ( (/) e. ( ~P a i^i Fin ) <-> ( (/) e. ~P a /\ (/) e. Fin ) )
19	16, 17, 18	mpbir2an 911	. . . . . . . . . 10 |- (/) e. ( ~P a i^i Fin )
20		unieq 4206	. . . . . . . . . . . . 13 |- ( b = (/) -> U. b = U. (/) )
21		uni0 4225	. . . . . . . . . . . . 13 |- U. (/) = (/)
22	20, 21	syl6eq 2511	. . . . . . . . . . . 12 |- ( b = (/) -> U. b = (/) )
23	22	eqeq2d 2468	. . . . . . . . . . 11 |- ( b = (/) -> ( X = U. b <-> X = (/) ) )
24	23	rspcev 3177	. . . . . . . . . 10 |- ( ( (/) e. ( ~P a i^i Fin ) /\ X = (/) ) -> E. b e. ( ~P a i^i Fin ) X = U. b )
25	19, 24	mpan 670	. . . . . . . . 9 |- ( X = (/) -> E. b e. ( ~P a i^i Fin ) X = U. b )
26	25	a1i13 28637	. . . . . . . 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 3753	. . . . . . . . 9 |- ( X =/= (/) <-> E. x x e. X )
28		simp2 989	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ X = U. a /\ a C_ J ) -> X = U. a )
29	28	eleq2d 2524	. . . . . . . . . . . . 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 4202	. . . . . . . . . . . 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 993	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> a C_ J )
34		simprl 755	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. a )
35	33, 34	sseldd 3464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
36		elssuni 4228	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. J -> s C_ U. J )
37	36, 2	syl6sseqr 3510	. . . . . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . . . . 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 4318	. . . . . . . . . . . . . . . . . 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 3633	. . . . . . . . . . . . . . . . 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 992	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> X = U. a )
45		uniiun 4330	. . . . . . . . . . . . . . . . . 18 |- U. a = U_ p e. a p
46	44, 45	syl6eq 2511	. . . . . . . . . . . . . . . . 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 3617	. . . . . . . . . . . . . . . 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 2497	. . . . . . . . . . . . . . 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 4358	. . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = ( U_ p e. a s u. U_ p e. a p )
50		vex 3079	. . . . . . . . . . . . . . . . . 18 |- s e. _V
51		vex 3079	. . . . . . . . . . . . . . . . . 18 |- p e. _V
52	50, 51	unex 6487	. . . . . . . . . . . . . . . . 17 |- ( s u. p ) e. _V
53	52	dfiun3 5201	. . . . . . . . . . . . . . . 16 |- U_ p e. a ( s u. p ) = U. ran ( p e. a |-> ( s u. p ) )
54	49, 53	eqtr3i 2485	. . . . . . . . . . . . . . 15 |- ( U_ p e. a s u. U_ p e. a p ) = U. ran ( p e. a |-> ( s u. p ) )
55	48, 54	syl6eq 2511	. . . . . . . . . . . . . 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 1027	. . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . 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 3463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) /\ p e. a ) -> p e. J )
59		unopn 18647	. . . . . . . . . . . . . . . . . . 19 |- ( ( J e. Top /\ s e. J /\ p e. J ) -> ( s u. p ) e. J )
60	56, 57, 58, 59	syl3anc 1219	. . . . . . . . . . . . . . . . . 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 2454	. . . . . . . . . . . . . . . . . 18 |- ( p e. a |-> ( s u. p ) ) = ( p e. a |-> ( s u. p ) )
62	60, 61	fmptd 5975	. . . . . . . . . . . . . . . . 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 5672	. . . . . . . . . . . . . . . . 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 4562	. . . . . . . . . . . . . . . . . 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 1009	. . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . 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 4206	. . . . . . . . . . . . . . . . . 18 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> U. c = U. ran ( p e. a |-> ( s u. p ) ) )
70	69	eqeq2d 2468	. . . . . . . . . . . . . . . . 17 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( X = U. c <-> X = U. ran ( p e. a |-> ( s u. p ) ) ) )
71		sseq2 3485	. . . . . . . . . . . . . . . . . . 19 |- ( c = ran ( p e. a |-> ( s u. p ) ) -> ( d C_ c <-> d C_ ran ( p e. a |-> ( s u. p ) ) ) )
72	71	anbi1d 704	. . . . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . . . . 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 3173	. . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. s )
79		ssel2 3458	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( a C_ J /\ s e. a ) -> s e. J )
80	79	3ad2antl3 1152	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ s e. a ) -> s e. J )
81	80	adantrr 716	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> s e. J )
82		elunii 4203	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. s /\ s e. J ) -> x e. U. J )
83	78, 81, 82	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. U. J )
84	83, 2	syl6eleqr 2553	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. X )
85	84	adantr 465	. . . . . . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . . 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 2544	. . . . . . . . . . . . . . . . . 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 2454	. . . . . . . . . . . . . . . . . . . 20 |- U. d = U. d
89	88	ptfinfin 28717	. . . . . . . . . . . . . . . . . . 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 755	. . . . . . . . . . . . . . . . . . . . 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 3630	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. s -> x e. ( s u. p ) )
94	93	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ X = U. a /\ a C_ J ) /\ ( s e. a /\ x e. s ) ) -> x e. ( s u. p ) )
95	94	ralrimivw 2830	. . . . . . . . . . . . . . . . . . . . . . 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 2899	. . . . . . . . . . . . . . . . . . . . . . . 24 |- A. p e. a ( s u. p ) e. _V
97		eleq2 2527	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = ( s u. p ) -> ( x e. z <-> x e. ( s u. p ) ) )
98	61, 97	ralrnmpt 5960	. . . . . . . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . . . 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 3523	. . . . . . . . . . . . . . . . . . . . 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 3002	. . . . . . . . . . . . . . . . . . . 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 2523	. . . . . . . . . . . . . . . . . 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 5192	. . . . . . . . . . . . . . . . . . . . 21 |- ran ( p e. a |-> ( s u. p ) ) = { q | E. p e. a q = ( s u. p ) }
109	92, 108	syl6sseq 3509	. . . . . . . . . . . . . . . . . . . 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 3530	. . . . . . . . . . . . . . . . . . . 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 3611	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = ( f ` q ) -> ( s u. p ) = ( s u. ( f ` q ) ) )
113	112	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . 21 |- ( p = ( f ` q ) -> ( q = ( s u. p ) <-> q = ( s u. ( f ` q ) ) ) )
114	113	ac6sfi 7666	. . . . . . . . . . . . . . . . . . . 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 5672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : d --> a -> ran f C_ a )
118	117	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f : d --> a /\ A. q e. d q = ( s u. ( f ` q ) ) ) -> ran f C_ a )
119	118	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . . . . . . 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 4125	. . . . . . . . . . . . . . . . . . . . . . . 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 3639	. . . . . . . . . . . . . . . . . . . . . . 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 755	. . . . . . . . . . . . . . . . . . . . . . . . 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 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 )
125		ffn 5666	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5733	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7707	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. Fin /\ f : d -onto-> ran f ) -> ran f e. Fin )
130	123, 128, 129	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 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 7499	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { s } e. Fin
132		unfi 7689	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran f e. Fin /\ { s } e. Fin ) -> ( ran f u. { s } ) e. Fin )
133	130, 131, 132	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . 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 7723	. . . . . . . . . . . . . . . . . . . . . . 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 664	. . . . . . . . . . . . . . . . . . . . . 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 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 )
137		uniiun 4330	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- U. d = U_ q e. d q
138		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 ) ) )
139		iuneq2 4294	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2507	. . . . . . . . . . . . . . . . . . . . . . . . 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 2495	. . . . . . . . . . . . . . . . . . . . . . . 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 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- { s } C_ ( ran f u. { s } )
144		ssnid 4013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- s e. { s }
145	143, 144	sselii 3460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- s e. ( ran f u. { s } )
146		elssuni 4228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5821	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f ` q ) C_ U. ran f
149		ssun1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ran f C_ ( ran f u. { s } )
150	149	unissi 4221	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- U. ran f C_ U. ( ran f u. { s } )
151	148, 150	sstri 3472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f ` q ) C_ U. ( ran f u. { s } )
152	147, 151	unssi 3638	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
153	152	rgenw 2899	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- A. q e. d ( s u. ( f ` q ) ) C_ U. ( ran f u. { s } )
154		iunss 4318	. . . . . . . . . . . . . . . . . . . . . . . . 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 3513	. . . . . . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3473	. . . . . . . . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4125	. . . . . . . . . . . . . . . . . . . . . . . . 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 3639	. . . . . . . . . . . . . . . . . . . . . . . 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 4219	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ran f u. { s } ) C_ J -> U. ( ran f u. { s } ) C_ U. J )
163	162, 2	syl6sseqr 3510	. . . . . . . . . . . . . . . . . . . . . . . 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 3480	. . . . . . . . . . . . . . . . . . . . . 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 4206	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b = ( ran f u. { s } ) -> U. b = U. ( ran f u. { s } ) )
167	166	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( b = ( ran f u. { s } ) -> ( X = U. b <-> X = U. ( ran f u. { s } ) ) )
168	167	rspcev 3177	. . . . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . . . 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 615	. . . . . . . . . . . . . . . . . . . 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 1691	. . . . . . . . . . . . . . . . . . 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 2944	. . . . . . . . . . . . 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 2946	. . . . . . . . . . 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 1691	. . . . . . . . 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 2768	. . . . . . 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 1254	. . . . . 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 1187	. . . . 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 2909	. . 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 19122	. . . 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 897	. . 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 965   = wceq 1370   E.wex 1587   e. wcel 1758   {cab 2439   =/= wne 2647   A.wral 2798   E.wrex 2799   {crab 2802   _Vcvv 3076   u. cun 3433   i^i cin 3434   C_ wss 3435   (/)c0 3744   ~Pcpw 3967   {csn 3984   U.cuni 4198   U_ciun 4278   |-> cmpt 4457   ran crn 4948   Fn wfn 5520   -->wf 5521   -onto->wfo 5523   ` cfv 5525   Fincfn 7419   Topctop 18629   Compccmp 19120   PtFincptfin 28680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-om 6586  df-recs 6941  df-rdg 6975  df-1o 7029  df-oadd 7033  df-er 7210  df-en 7420  df-dom 7421  df-fin 7423  df-top 18634  df-cmp 19121  df-ptfin 28684

This theorem is referenced by: (None)