Theorem comppfsc 15517

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.

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

Proof of Theorem comppfsc

Step	Hyp	Ref	Expression
1		comppfsc.1	. . . . . . 7 |- X = U.J
2	1	compcov 15429	. . . . . 6 |- ((J e. Comp /\ c C_ J /\ X = U.c) -> E.d e. (~Pc i^i Fin)X = U.d)
3		finptfin 15507	. . . . . . . . . 10 |- (d e. Fin -> d e. PtFin)
4	3	ad2antlr 441	. . . . . . . . 9 |- (((d C_ c /\ d e. Fin) /\ X = U.d) -> d e. PtFin)
5		simpll 448	. . . . . . . . 9 |- (((d C_ c /\ d e. Fin) /\ X = U.d) -> d C_ c)
6		simpr 350	. . . . . . . . 9 |- (((d C_ c /\ d e. Fin) /\ X = U.d) -> X = U.d)
7	4, 5, 6	jca32 312	. . . . . . . 8 |- (((d C_ c /\ d e. Fin) /\ X = U.d) -> (d e. PtFin /\ (d C_ c /\ X = U.d)))
8		elin 2786	. . . . . . . . 9 |- (d e. (~Pc i^i Fin) <-> (d e. ~Pc /\ d e. Fin))
9		visset 2295	. . . . . . . . . . 11 |- d e. _V
10	9	elpw 3037	. . . . . . . . . 10 |- (d e. ~Pc <-> d C_ c)
11	10	anbi1i 539	. . . . . . . . 9 |- ((d e. ~Pc /\ d e. Fin) <-> (d C_ c /\ d e. Fin))
12	8, 11	bitri 190	. . . . . . . 8 |- (d e. (~Pc i^i Fin) <-> (d C_ c /\ d e. Fin))
13	7, 12	sylanb 498	. . . . . . 7 |- ((d e. (~Pc i^i Fin) /\ X = U.d) -> (d e. PtFin /\ (d C_ c /\ X = U.d)))
14	13	reximi2 2197	. . . . . 6 |- (E.d e. (~Pc i^i Fin)X = U.d -> E.d e. PtFin (d C_ c /\ X = U.d))
15	2, 14	syl 12	. . . . 5 |- ((J e. Comp /\ c C_ J /\ X = U.c) -> E.d e. PtFin (d C_ c /\ X = U.d))
16		visset 2295	. . . . . 6 |- c e. _V
17	16	elpw 3037	. . . . 5 |- (c e. ~PJ <-> c C_ J)
18	15, 17	syl3an2b 1134	. . . 4 |- ((J e. Comp /\ c e. ~PJ /\ X = U.c) -> E.d e. PtFin (d C_ c /\ X = U.d))
19	18	3exp 1066	. . 3 |- (J e. Comp -> (c e. ~PJ -> (X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d))))
20	19	r19.21aiv 2175	. 2 |- (J e. Comp -> A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)))
21		elin 2786	. . . . . . . . . . 11 |- ((/) e. (~Pa i^i Fin) <-> ((/) e. ~Pa /\ (/) e. Fin))
22		0elpw 3473	. . . . . . . . . . 11 |- (/) e. ~Pa
23		emfin 10165	. . . . . . . . . . 11 |- (/) e. Fin
24	21, 22, 23	mpbir2an 800	. . . . . . . . . 10 |- (/) e. (~Pa i^i Fin)
25	24	a1i 8	. . . . . . . . 9 |- (X = (/) -> (/) e. (~Pa i^i Fin))
26	1	eqeq1i 1891	. . . . . . . . . 10 |- (X = (/) <-> U.J = (/))
27	26	biimpi 168	. . . . . . . . 9 |- (X = (/) -> U.J = (/))
28		unieq 3185	. . . . . . . . . . . 12 |- (b = (/) -> U.b = U.(/))
29		uni0 3205	. . . . . . . . . . . 12 |- U.(/) = (/)
30	28, 29	syl6eq 1944	. . . . . . . . . . 11 |- (b = (/) -> U.b = (/))
31	30	eqeq2d 1895	. . . . . . . . . 10 |- (b = (/) -> (U.J = U.b <-> U.J = (/)))
32	31	rcla4ev 2381	. . . . . . . . 9 |- (((/) e. (~Pa i^i Fin) /\ U.J = (/)) -> E.b e. (~Pa i^i Fin)U.J = U.b)
33	25, 27, 32	syl11anc 524	. . . . . . . 8 |- (X = (/) -> E.b e. (~Pa i^i Fin)U.J = U.b)
34	33	a1i13 15326	. . . . . . 7 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (X = (/) -> (A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) -> E.b e. (~Pa i^i Fin)U.J = U.b)))
35	1	eqeq1i 1891	. . . . . . . . . . . . . . 15 |- (X = U.a <-> U.J = U.a)
36	35	biimpri 169	. . . . . . . . . . . . . 14 |- (U.J = U.a -> X = U.a)
37	36	eleq2d 1964	. . . . . . . . . . . . 13 |- (U.J = U.a -> (x e. X <-> x e. U.a))
38	37	biimpd 170	. . . . . . . . . . . 12 |- (U.J = U.a -> (x e. X -> x e. U.a))
39	38	3ad2ant2 898	. . . . . . . . . . 11 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (x e. X -> x e. U.a))
40		eluni2 3181	. . . . . . . . . . 11 |- (x e. U.a <-> E.s e. a x e. s)
41	39, 40	syl6ib 229	. . . . . . . . . 10 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (x e. X -> E.s e. a x e. s))
42	36	3ad2ant2 898	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> X = U.a)
43	42	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> X = U.a)
44		elun2 2772	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. q -> y e. (s u. q))
45	44	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (y e. q /\ q e. a)) -> y e. (s u. q))
46		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (s u. q) = (s u. q)
47		uneq2 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (p = q -> (s u. p) = (s u. q))
48	47	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (p = q -> ((s u. q) = (s u. p) <-> (s u. q) = (s u. q)))
49	48	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((q e. a /\ (s u. q) = (s u. q)) -> E.p e. a (s u. q) = (s u. p))
50	46, 49	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (q e. a -> E.p e. a (s u. q) = (s u. p))
51	50	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (y e. q /\ q e. a)) -> E.p e. a (s u. q) = (s u. p))
52		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- s e. _V
53		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- q e. _V
54	52, 53	unex 3796	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (s u. q) e. _V
55		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t = (s u. q) -> (y e. t <-> y e. (s u. q)))
56		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t = (s u. q) -> (t = (s u. p) <-> (s u. q) = (s u. p)))
57	56	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t = (s u. q) -> (E.p e. a t = (s u. p) <-> E.p e. a (s u. q) = (s u. p)))
58	55, 57	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t = (s u. q) -> ((y e. t /\ E.p e. a t = (s u. p)) <-> (y e. (s u. q) /\ E.p e. a (s u. q) = (s u. p))))
59	54, 58	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. (s u. q) /\ E.p e. a (s u. q) = (s u. p)) -> E.t(y e. t /\ E.p e. a t = (s u. p)))
60	45, 51, 59	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (y e. q /\ q e. a)) -> E.t(y e. t /\ E.p e. a t = (s u. p)))
61	60	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> ((y e. q /\ q e. a) -> E.t(y e. t /\ E.p e. a t = (s u. p))))
62	61	19.23adv 1584	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (E.q(y e. q /\ q e. a) -> E.t(y e. t /\ E.p e. a t = (s u. p))))
63		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t = (s u. p) -> (y e. t <-> y e. (s u. p)))
64	63	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (t = (s u. p) /\ p e. a)) -> (y e. t <-> y e. (s u. p)))
65		elun 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y e. (s u. p) <-> (y e. s \/ y e. p))
66	64, 65	syl6bb 595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (t = (s u. p) /\ p e. a)) -> (y e. t <-> (y e. s \/ y e. p)))
67		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (q = s -> (y e. q <-> y e. s))
68		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (q = s -> (q e. a <-> s e. a))
69	67, 68	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (q = s -> ((y e. q /\ q e. a) <-> (y e. s /\ s e. a)))
70	52, 69	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((y e. s /\ s e. a) -> E.q(y e. q /\ q e. a))
71	70	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (s e. a -> (y e. s -> E.q(y e. q /\ q e. a)))
72	71	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((s e. a /\ x e. s) -> (y e. s -> E.q(y e. q /\ q e. a)))
73	72	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ p e. a) -> (y e. s -> E.q(y e. q /\ q e. a)))
74		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- p e. _V
75		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (q = p -> (y e. q <-> y e. p))
76		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (q = p -> (q e. a <-> p e. a))
77	75, 76	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (q = p -> ((y e. q /\ q e. a) <-> (y e. p /\ p e. a)))
78	74, 77	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((y e. p /\ p e. a) -> E.q(y e. q /\ q e. a))
79	78	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (p e. a -> (y e. p -> E.q(y e. q /\ q e. a)))
80	79	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ p e. a) -> (y e. p -> E.q(y e. q /\ q e. a)))
81	73, 80	jaod 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ p e. a) -> ((y e. s \/ y e. p) -> E.q(y e. q /\ q e. a)))
82	81	adantrl 430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (t = (s u. p) /\ p e. a)) -> ((y e. s \/ y e. p) -> E.q(y e. q /\ q e. a)))
83	66, 82	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (t = (s u. p) /\ p e. a)) -> (y e. t -> E.q(y e. q /\ q e. a)))
84	83	exp32 408	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (t = (s u. p) -> (p e. a -> (y e. t -> E.q(y e. q /\ q e. a)))))
85	84	com23 36	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (p e. a -> (t = (s u. p) -> (y e. t -> E.q(y e. q /\ q e. a)))))
86	85	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (E.p e. a t = (s u. p) -> (y e. t -> E.q(y e. q /\ q e. a))))
87	86	com23 36	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (y e. t -> (E.p e. a t = (s u. p) -> E.q(y e. q /\ q e. a))))
88	87	imp3a 388	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> ((y e. t /\ E.p e. a t = (s u. p)) -> E.q(y e. q /\ q e. a)))
89	88	19.23adv 1584	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (E.t(y e. t /\ E.p e. a t = (s u. p)) -> E.q(y e. q /\ q e. a)))
90	62, 89	impbid 574	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (E.q(y e. q /\ q e. a) <-> E.t(y e. t /\ E.p e. a t = (s u. p))))
91		eluni 3180	. . . . . . . . . . . . . . . . . . 19 |- (y e. U.a <-> E.q(y e. q /\ q e. a))
92		eluniab 3189	. . . . . . . . . . . . . . . . . . 19 |- (y e. U.{t | E.p e. a t = (s u. p)} <-> E.t(y e. t /\ E.p e. a t = (s u. p)))
93	90, 91, 92	3bitr4g 614	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (y e. U.a <-> y e. U.{t | E.p e. a t = (s u. p)}))
94	93	eqrdv 1882	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> U.a = U.{t | E.p e. a t = (s u. p)})
95	43, 94	eqtrd 1925	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> X = U.{t | E.p e. a t = (s u. p)})
96		simprr 451	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (p e. a /\ t = (s u. p))) -> t = (s u. p))
97		simpll1 915	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (p e. a /\ t = (s u. p))) -> J e. Top)
98		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- a e. _V
99	98	elpw 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (a e. ~PJ <-> a C_ J)
100		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (a C_ J -> (s e. a -> s e. J))
101		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (a C_ J -> (p e. a -> p e. J))
102	100, 101	anim12d 617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (a C_ J -> ((s e. a /\ p e. a) -> (s e. J /\ p e. J)))
103	102	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (a C_ J -> (s e. a -> (p e. a -> (s e. J /\ p e. J))))
104	99, 103	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a e. ~PJ -> (s e. a -> (p e. a -> (s e. J /\ p e. J))))
105	104	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (s e. a -> (p e. a -> (s e. J /\ p e. J))))
106	105	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ s e. a) /\ p e. a) -> (s e. J /\ p e. J))
107	106	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ p e. a) -> (s e. J /\ p e. J))
108	107	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (p e. a /\ t = (s u. p))) -> (s e. J /\ p e. J))
109	52, 74	prss 3138	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((s e. J /\ p e. J) <-> {s, p} C_ J)
110	108, 109	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (p e. a /\ t = (s u. p))) -> {s, p} C_ J)
111		uniopn 8867	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ {s, p} C_ J) -> U.{s, p} e. J)
112	97, 110, 111	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (p e. a /\ t = (s u. p))) -> U.{s, p} e. J)
113	52, 74	unipr 3191	. . . . . . . . . . . . . . . . . . . . . . 23 |- U.{s, p} = (s u. p)
114	112, 113	syl5eqelr 1976	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (p e. a /\ t = (s u. p))) -> (s u. p) e. J)
115	96, 114	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (p e. a /\ t = (s u. p))) -> t e. J)
116	115	exp32 408	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (p e. a -> (t = (s u. p) -> t e. J)))
117	116	r19.23adv 2215	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (E.p e. a t = (s u. p) -> t e. J))
118	117	abssdv 2681	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> {t | E.p e. a t = (s u. p)} C_ J)
119		elpw2g 3463	. . . . . . . . . . . . . . . . . . . 20 |- (J e. Top -> ({t | E.p e. a t = (s u. p)} e. ~PJ <-> {t | E.p e. a t = (s u. p)} C_ J))
120	119	3ad2ant1 897	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> ({t | E.p e. a t = (s u. p)} e. ~PJ <-> {t | E.p e. a t = (s u. p)} C_ J))
121	120	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> ({t | E.p e. a t = (s u. p)} e. ~PJ <-> {t | E.p e. a t = (s u. p)} C_ J))
122	118, 121	mpbird 213	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> {t | E.p e. a t = (s u. p)} e. ~PJ)
123		unieq 3185	. . . . . . . . . . . . . . . . . . . 20 |- (c = {t | E.p e. a t = (s u. p)} -> U.c = U.{t | E.p e. a t = (s u. p)})
124	123	eqeq2d 1895	. . . . . . . . . . . . . . . . . . 19 |- (c = {t | E.p e. a t = (s u. p)} -> (X = U.c <-> X = U.{t | E.p e. a t = (s u. p)}))
125		sseq2 2639	. . . . . . . . . . . . . . . . . . . . 21 |- (c = {t | E.p e. a t = (s u. p)} -> (d C_ c <-> d C_ {t | E.p e. a t = (s u. p)}))
126	125	anbi1d 679	. . . . . . . . . . . . . . . . . . . 20 |- (c = {t | E.p e. a t = (s u. p)} -> ((d C_ c /\ X = U.d) <-> (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)))
127	126	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (c = {t | E.p e. a t = (s u. p)} -> (E.d e. PtFin (d C_ c /\ X = U.d) <-> E.d e. PtFin (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)))
128	124, 127	imbi12d 688	. . . . . . . . . . . . . . . . . 18 |- (c = {t | E.p e. a t = (s u. p)} -> ((X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) <-> (X = U.{t | E.p e. a t = (s u. p)} -> E.d e. PtFin (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d))))
129	128	rcla4v 2376	. . . . . . . . . . . . . . . . 17 |- ({t | E.p e. a t = (s u. p)} e. ~PJ -> (A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) -> (X = U.{t | E.p e. a t = (s u. p)} -> E.d e. PtFin (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d))))
130	122, 129	syl 12	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (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.{t | E.p e. a t = (s u. p)} -> E.d e. PtFin (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d))))
131	95, 130	mpid 58	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (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_ {t | E.p e. a t = (s u. p)} /\ X = U.d)))
132		simprr 451	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> x e. s)
133		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((a C_ J /\ s e. a) -> s e. J)
134	133, 99	sylanb 498	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a e. ~PJ /\ s e. a) -> s e. J)
135	134	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a e. ~PJ /\ (s e. a /\ x e. s)) -> s e. J)
136	135	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> s e. J)
137		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. s /\ s e. J) -> x e. U.J)
138	132, 136, 137	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> x e. U.J)
139	138	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> x e. U.J)
140		simprr 451	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> X = U.d)
141	140, 1	syl5eqr 1942	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> U.J = U.d)
142	139, 141	eleqtrd 1973	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> x e. U.d)
143		eqid 1884	. . . . . . . . . . . . . . . . . . . . . 22 |- U.d = U.d
144	143	ptfinfin 15508	. . . . . . . . . . . . . . . . . . . . 21 |- ((d e. PtFin /\ x e. U.d) -> {z e. d | x e. z} e. Fin)
145	144	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (x e. U.d -> (d e. PtFin -> {z e. d | x e. z} e. Fin))
146	142, 145	syl 12	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> (d e. PtFin -> {z e. d | x e. z} e. Fin))
147		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (d C_ {t | E.p e. a t = (s u. p)} -> (z e. d -> z e. {t | E.p e. a t = (s u. p)}))
148		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (z = (s u. p) -> (x e. z <-> x e. (s u. p)))
149		elun1 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x e. s -> x e. (s u. p))
150	149	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> x e. (s u. p))
151	148, 150	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (z = (s u. p) -> x e. z))
152	151	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (p e. a -> (z = (s u. p) -> x e. z)))
153	152	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (E.p e. a z = (s u. p) -> x e. z))
154		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- z e. _V
155		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = z -> (t = (s u. p) <-> z = (s u. p)))
156	155	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = z -> (E.p e. a t = (s u. p) <-> E.p e. a z = (s u. p)))
157	154, 156	elab 2403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. {t | E.p e. a t = (s u. p)} <-> E.p e. a z = (s u. p))
158	153, 157	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (z e. {t | E.p e. a t = (s u. p)} -> x e. z))
159	147, 158	sylan9r 519	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ d C_ {t | E.p e. a t = (s u. p)}) -> (z e. d -> x e. z))
160	159	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> (z e. d -> x e. z))
161	160	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> A.z e. d x e. z)
162		ssid 2634	. . . . . . . . . . . . . . . . . . . . . 22 |- d C_ d
163	161, 162	jctil 316	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> (d C_ d /\ A.z e. d x e. z))
164		ssrab 2685	. . . . . . . . . . . . . . . . . . . . 21 |- (d C_ {z e. d | x e. z} <-> (d C_ d /\ A.z e. d x e. z))
165	163, 164	sylibr 217	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> d C_ {z e. d | x e. z})
166		ssfi 5630	. . . . . . . . . . . . . . . . . . . . 21 |- (({z e. d | x e. z} e. Fin /\ d C_ {z e. d | x e. z}) -> d e. Fin)
167	166	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (d C_ {z e. d | x e. z} -> ({z e. d | x e. z} e. Fin -> d e. Fin))
168	165, 167	syl 12	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> ({z e. d | x e. z} e. Fin -> d e. Fin))
169		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (d C_ {t | E.p e. a t = (s u. p)} -> (q e. d -> q e. {t | E.p e. a t = (s u. p)}))
170		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t = q -> (t = (s u. p) <-> q = (s u. p)))
171	170	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t = q -> (E.p e. a t = (s u. p) <-> E.p e. a q = (s u. p)))
172	53, 171	elab 2403	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (q e. {t | E.p e. a t = (s u. p)} <-> E.p e. a q = (s u. p))
173	169, 172	syl6ib 229	. . . . . . . . . . . . . . . . . . . . . . 23 |- (d C_ {t | E.p e. a t = (s u. p)} -> (q e. d -> E.p e. a q = (s u. p)))
174	173	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . 22 |- (d C_ {t | E.p e. a t = (s u. p)} -> A.q e. d E.p e. a q = (s u. p))
175	174	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> A.q e. d E.p e. a q = (s u. p))
176		uneq2 2749	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (p = (f` q) -> (s u. p) = (s u. (f` q)))
177	176	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . 23 |- (p = (f` q) -> (q = (s u. p) <-> q = (s u. (f` q))))
178	177	ac6sfi 5509	. . . . . . . . . . . . . . . . . . . . . 22 |- ((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))))
179	178	expcom 403	. . . . . . . . . . . . . . . . . . . . 21 |- (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)))))
180	175, 179	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> (d e. Fin -> E.f(f:d-->a /\ A.q e. d q = (s u. (f` q)))))
181		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((ran f u. {s}) e. (~Pa i^i Fin) <-> ((ran f u. {s}) e. ~Pa /\ (ran f u. {s}) e. Fin))
182	98	elpw2 3464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((ran f u. {s}) e. ~Pa <-> (ran f u. {s}) C_ a)
183	182	anbi1i 539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((ran f u. {s}) e. ~Pa /\ (ran f u. {s}) e. Fin) <-> ((ran f u. {s}) C_ a /\ (ran f u. {s}) e. Fin))
184	181, 183	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((ran f u. {s}) e. (~Pa i^i Fin) <-> ((ran f u. {s}) C_ a /\ (ran f u. {s}) e. Fin))
185		frn 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:d-->a -> ran f C_ a)
186	185	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f:d-->a /\ A.q e. d q = (s u. (f` q))) -> ran f C_ a)
187	186	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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)
188		snssi 3129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (s e. a -> {s} C_ a)
189	188	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> {s} C_ a)
190	189	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> {s} C_ a)
191	187, 190	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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 /\ {s} C_ a))
192		unss 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((ran f C_ a /\ {s} C_ a) <-> (ran f u. {s}) C_ a)
193	191, 192	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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)
194		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> d e. Fin)
195		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:d-->a -> f Fn d)
196		dffn4 4623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f Fn d <-> f:d-onto->ran f)
197	195, 196	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:d-->a -> f:d-onto->ran f)
198	197	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:d-->a /\ A.q e. d q = (s u. (f` q))) -> f:d-onto->ran f)
199	198	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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)
200		fodomfi 5656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((d e. Fin /\ f:d-onto->ran f) -> ran f ~<_ d)
201	194, 199, 200	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> ran f ~<_ d)
202		domfi 5631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((d e. Fin /\ ran f ~<_ d) -> ran f e. Fin)
203	194, 201, 202	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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)
204		snfi 5491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {s} e. Fin
205		unfi 5644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((ran f e. Fin /\ {s} e. Fin) -> (ran f u. {s}) e. Fin)
206	204, 205	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (ran f e. Fin -> (ran f u. {s}) e. Fin)
207	203, 206	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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)
208	184, 193, 207	sylanbrc 527	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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. (~Pa i^i Fin))
209		simplrr 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> X = U.d)
210	209, 1	syl5eqr 1942	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> U.J = U.d)
211		id 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (q = z -> q = z)
212		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (q = z -> (f` q) = (f` z))
213	212	uneq2d 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (q = z -> (s u. (f` q)) = (s u. (f` z)))
214	211, 213	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (q = z -> (q = (s u. (f` q)) <-> z = (s u. (f` z))))
215	214	rcla4cv 2377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (A.q e. d q = (s u. (f` q)) -> (z e. d -> z = (s u. (f` z))))
216	215	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f:d-->a /\ A.q e. d q = (s u. (f` q))) -> (z e. d -> z = (s u. (f` z))))
217	216	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> (z e. d -> z = (s u. (f` z))))
218		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (z = (s u. (f` z)) -> (y e. z <-> y e. (s u. (f` z))))
219	218	imbi1d 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z = (s u. (f` z)) -> ((y e. z -> y e. U.(ran f u. {s})) <-> (y e. (s u. (f` z)) -> y e. U.(ran f u. {s}))))
220	52	snid 3069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- s e. {s}
221		elun2 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (s e. {s} -> s e. (ran f u. {s}))
222	220, 221	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- s e. (ran f u. {s})
223		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((y e. s /\ s e. (ran f u. {s})) -> y e. U.(ran f u. {s}))
224	222, 223	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (y e. s -> y e. U.(ran f u. {s}))
225	224	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) /\ z e. d) -> (y e. s -> y e. U.(ran f u. {s})))
226		fnfvelrn 4786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((f Fn d /\ z e. d) -> (f` z) e. ran f)
227	226	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (f Fn d -> (z e. d -> (f` z) e. ran f))
228		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((y e. (f` z) /\ (f` z) e. ran f) -> y e. U.ran f)
229		ssun1 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ran f C_ (ran f u. {s})
230		uniss 3199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (ran f C_ (ran f u. {s}) -> U.ran f C_ U.(ran f u. {s}))
231	229, 230	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- U.ran f C_ U.(ran f u. {s})
232	231	sseli 2617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y e. U.ran f -> y e. U.(ran f u. {s}))
233	228, 232	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((y e. (f` z) /\ (f` z) e. ran f) -> y e. U.(ran f u. {s}))
234	233	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((f` z) e. ran f -> (y e. (f` z) -> y e. U.(ran f u. {s})))
235	227, 234	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (f Fn d -> (z e. d -> (y e. (f` z) -> y e. U.(ran f u. {s}))))
236	195, 235	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (f:d-->a -> (z e. d -> (y e. (f` z) -> y e. U.(ran f u. {s}))))
237	236	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((f:d-->a /\ A.q e. d q = (s u. (f` q))) -> (z e. d -> (y e. (f` z) -> y e. U.(ran f u. {s}))))
238	237	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> (z e. d -> (y e. (f` z) -> y e. U.(ran f u. {s}))))
239	238	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) /\ z e. d) -> (y e. (f` z) -> y e. U.(ran f u. {s})))
240	225, 239	jaod 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) /\ z e. d) -> ((y e. s \/ y e. (f` z)) -> y e. U.(ran f u. {s})))
241		elun 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (y e. (s u. (f` z)) <-> (y e. s \/ y e. (f` z)))
242	240, 241	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) /\ z e. d) -> (y e. (s u. (f` z)) -> y e. U.(ran f u. {s})))
243	219, 242	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) /\ z e. d) -> (z = (s u. (f` z)) -> (y e. z -> y e. U.(ran f u. {s}))))
244	243	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> (z e. d -> (z = (s u. (f` z)) -> (y e. z -> y e. U.(ran f u. {s})))))
245	217, 244	mpdd 57	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> (z e. d -> (y e. z -> y e. U.(ran f u. {s}))))
246	245	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> (y e. z -> (z e. d -> y e. U.(ran f u. {s}))))
247	246	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> ((y e. z /\ z e. d) -> y e. U.(ran f u. {s})))
248	247	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> (E.z(y e. z /\ z e. d) -> y e. U.(ran f u. {s})))
249		eluni 3180	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y e. U.d <-> E.z(y e. z /\ z e. d))
250	248, 249	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> (y e. U.d -> y e. U.(ran f u. {s})))
251	250	ssrdv 2622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> U.d C_ U.(ran f u. {s}))
252	210, 251	eqsstrd 2651	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> U.J C_ U.(ran f u. {s}))
253		elpwi 3039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (a e. ~PJ -> a C_ J)
254	253	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> a C_ J)
255	254	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> a C_ J)
256	255	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> a C_ J)
257	187, 256	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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)
258	133	snssd 3130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((a C_ J /\ s e. a) -> {s} C_ J)
259	258, 99	sylanb 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((a e. ~PJ /\ s e. a) -> {s} C_ J)
260	259	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((a e. ~PJ /\ (s e. a /\ x e. s)) -> {s} C_ J)
261	260	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> {s} C_ J)
262	261	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> {s} C_ J)
263	257, 262	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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 /\ {s} C_ J))
264		unss 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((ran f C_ J /\ {s} C_ J) <-> (ran f u. {s}) C_ J)
265	263, 264	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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)
266		uniss 3199	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((ran f u. {s}) C_ J -> U.(ran f u. {s}) C_ U.J)
267	265, 266	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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_ U.J)
268	252, 267	eqssd 2633	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> U.J = U.(ran f u. {s}))
269		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b = (ran f u. {s}) -> U.b = U.(ran f u. {s}))
270	269	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (b = (ran f u. {s}) -> (U.J = U.b <-> U.J = U.(ran f u. {s})))
271	270	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((ran f u. {s}) e. (~Pa i^i Fin) /\ U.J = U.(ran f u. {s})) -> E.b e. (~Pa i^i Fin)U.J = U.b)
272	208, 268, 271	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ (d e. Fin /\ (f:d-->a /\ A.q e. d q = (s u. (f` q))))) -> E.b e. (~Pa i^i Fin)U.J = U.b)
273	272	expr 418	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) /\ d e. Fin) -> ((f:d-->a /\ A.q e. d q = (s u. (f` q))) -> E.b e. (~Pa i^i Fin)U.J = U.b))
274	273	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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. (~Pa i^i Fin)U.J = U.b))
275	274	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (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. (~Pa i^i Fin)U.J = U.b)))
276	180, 275	mpdd 57	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> (d e. Fin -> E.b e. (~Pa i^i Fin)U.J = U.b))
277	146, 168, 276	3syld 31	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) /\ (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d)) -> (d e. PtFin -> E.b e. (~Pa i^i Fin)U.J = U.b))
278	277	ex 402	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> ((d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d) -> (d e. PtFin -> E.b e. (~Pa i^i Fin)U.J = U.b)))
279	278	com23 36	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (d e. PtFin -> ((d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d) -> E.b e. (~Pa i^i Fin)U.J = U.b)))
280	279	r19.23adv 2215	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (s e. a /\ x e. s)) -> (E.d e. PtFin (d C_ {t | E.p e. a t = (s u. p)} /\ X = U.d) -> E.b e. (~Pa i^i Fin)U.J = U.b))
281	131, 280	syld 30	. . . . . . . . . . . . . 14 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ (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. (~Pa i^i Fin)U.J = U.b))
282	281	exp32 408	. . . . . . . . . . . . 13 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (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. (~Pa i^i Fin)U.J = U.b))))
283	282	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ x e. X) -> (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. (~Pa i^i Fin)U.J = U.b))))
284	283	r19.23adv 2215	. . . . . . . . . . 11 |- (((J e. Top /\ U.J = U.a /\ a e. ~PJ) /\ x e. X) -> (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. (~Pa i^i Fin)U.J = U.b)))
285	284	ex 402	. . . . . . . . . 10 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (x e. X -> (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. (~Pa i^i Fin)U.J = U.b))))
286	41, 285	mpdd 57	. . . . . . . . 9 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (x e. X -> (A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) -> E.b e. (~Pa i^i Fin)U.J = U.b)))
287	286	19.23adv 1584	. . . . . . . 8 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (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. (~Pa i^i Fin)U.J = U.b)))
288		n0 2884	. . . . . . . 8 |- (X =/= (/) <-> E.x x e. X)
289	287, 288	syl5ib 223	. . . . . . 7 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (X =/= (/) -> (A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) -> E.b e. (~Pa i^i Fin)U.J = U.b)))
290	34, 289	pm2.61dne 2091	. . . . . 6 |- ((J e. Top /\ U.J = U.a /\ a e. ~PJ) -> (A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) -> E.b e. (~Pa i^i Fin)U.J = U.b))
291	290	3exp 1066	. . . . 5 |- (J e. Top -> (U.J = U.a -> (a e. ~PJ -> (A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) -> E.b e. (~Pa i^i Fin)U.J = U.b))))
292	291	com24 41	. . . 4 |- (J e. Top -> (A.c e. ~P J(X = U.c -> E.d e. PtFin (d C_ c /\ X = U.d)) -> (a e. ~PJ -> (U.J = U.a -> E.b e. (~Pa i^i Fin)U.J = U.b))))
293	292	r19.21adv 2181	. . 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(U.J = U.a -> E.b e. (~Pa i^i Fin)U.J = U.b)))
294		iscomp 10330	. . . 4 |- (J e. Comp <-> (J e. Top /\ A.a e. ~P J(U.J = U.a -> E.b e. (~Pa i^i Fin)U.J = U.b)))
295	294	baibr 750	. . 3 |- (J e. Top -> (A.a e. ~P J(U.J = U.a -> E.b e. (~Pa i^i Fin)U.J = U.b) <-> J e. Comp))
296	293, 295	sylibd 219	. 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))
297	20, 296	impbid2 576	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 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  {cpr 3045  U.cuni 3177   class class class wbr 3338  ran crn 3987   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998   ~<_ cdom 5424  Fincfn 5426  Topctop 8857  Compccomp 10328  PtFincptfin 15459

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-top 8861  df-comp 10329  df-ptfin 15465

Copyright terms: Public domain