Theorem hauscmplem 21209

Description: Lemma for hauscmp 21210. (Contributed by Mario Carneiro, 27-Nov-2013.)

Hypotheses

Ref	Expression
hauscmp.1	|- X = U. J
hauscmplem.2	|- O = { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) }
hauscmplem.3	|- ( ph -> J e. Haus )
hauscmplem.4	|- ( ph -> S C_ X )
hauscmplem.5	|- ( ph -> ( J ↾t S ) e. Comp )
hauscmplem.6	|- ( ph -> A e. ( X \ S ) )

Assertion

Ref	Expression
hauscmplem	|- ( ph -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )

Distinct variable groups:   y, w, z, A   w, J, y, z   ph, w, y, z   w, S, y, z   z, O   w, X, y, z

Allowed substitution hints:   O( y, w)

Proof of Theorem hauscmplem

Dummy variables f x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hauscmplem.3	. . . . . . 7 |- ( ph -> J e. Haus )
2		haustop 21135	. . . . . . 7 |- ( J e. Haus -> J e. Top )
3	1, 2	syl 17	. . . . . 6 |- ( ph -> J e. Top )
4	3	ad3antrrr 766	. . . . 5 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> J e. Top )
5		hauscmp.1	. . . . . 6 |- X = U. J
6	5	topopn 20711	. . . . 5 |- ( J e. Top -> X e. J )
7	4, 6	syl 17	. . . 4 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> X e. J )
8		hauscmplem.6	. . . . . 6 |- ( ph -> A e. ( X \ S ) )
9	8	eldifad 3586	. . . . 5 |- ( ph -> A e. X )
10	9	ad3antrrr 766	. . . 4 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> A e. X )
11	5	clstop 20873	. . . . . . 7 |- ( J e. Top -> ( ( cls ` J ) ` X ) = X )
12	4, 11	syl 17	. . . . . 6 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( ( cls ` J ) ` X ) = X )
13		simplr 792	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> S C_ U. x )
14		unieq 4444	. . . . . . . . . . . 12 |- ( x = (/) -> U. x = U. (/) )
15		uni0 4465	. . . . . . . . . . . 12 |- U. (/) = (/)
16	14, 15	syl6eq 2672	. . . . . . . . . . 11 |- ( x = (/) -> U. x = (/) )
17	16	adantl 482	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> U. x = (/) )
18	13, 17	sseqtrd 3641	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> S C_ (/) )
19		ss0 3974	. . . . . . . . 9 |- ( S C_ (/) -> S = (/) )
20	18, 19	syl 17	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> S = (/) )
21	20	difeq2d 3728	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( X \ S ) = ( X \ (/) ) )
22		dif0 3950	. . . . . . 7 |- ( X \ (/) ) = X
23	21, 22	syl6eq 2672	. . . . . 6 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( X \ S ) = X )
24	12, 23	eqtr4d 2659	. . . . 5 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( ( cls ` J ) ` X ) = ( X \ S ) )
25		eqimss 3657	. . . . 5 |- ( ( ( cls ` J ) ` X ) = ( X \ S ) -> ( ( cls ` J ) ` X ) C_ ( X \ S ) )
26	24, 25	syl 17	. . . 4 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( ( cls ` J ) ` X ) C_ ( X \ S ) )
27		eleq2 2690	. . . . . 6 |- ( z = X -> ( A e. z <-> A e. X ) )
28		fveq2 6191	. . . . . . 7 |- ( z = X -> ( ( cls ` J ) ` z ) = ( ( cls ` J ) ` X ) )
29	28	sseq1d 3632	. . . . . 6 |- ( z = X -> ( ( ( cls ` J ) ` z ) C_ ( X \ S ) <-> ( ( cls ` J ) ` X ) C_ ( X \ S ) ) )
30	27, 29	anbi12d 747	. . . . 5 |- ( z = X -> ( ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) <-> ( A e. X /\ ( ( cls ` J ) ` X ) C_ ( X \ S ) ) ) )
31	30	rspcev 3309	. . . 4 |- ( ( X e. J /\ ( A e. X /\ ( ( cls ` J ) ` X ) C_ ( X \ S ) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
32	7, 10, 26, 31	syl12anc 1324	. . 3 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
33		elin 3796	. . . . . . 7 |- ( x e. ( ~P O i^i Fin ) <-> ( x e. ~P O /\ x e. Fin ) )
34		id 22	. . . . . . . 8 |- ( x e. Fin -> x e. Fin )
35		elpwi 4168	. . . . . . . . . . 11 |- ( x e. ~P O -> x C_ O )
36	35	sseld 3602	. . . . . . . . . 10 |- ( x e. ~P O -> ( z e. x -> z e. O ) )
37		difeq2 3722	. . . . . . . . . . . . . . 15 |- ( y = z -> ( X \ y ) = ( X \ z ) )
38	37	sseq2d 3633	. . . . . . . . . . . . . 14 |- ( y = z -> ( ( ( cls ` J ) ` w ) C_ ( X \ y ) <-> ( ( cls ` J ) ` w ) C_ ( X \ z ) ) )
39	38	anbi2d 740	. . . . . . . . . . . . 13 |- ( y = z -> ( ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) <-> ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
40	39	rexbidv 3052	. . . . . . . . . . . 12 |- ( y = z -> ( E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) <-> E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
41		hauscmplem.2	. . . . . . . . . . . 12 |- O = { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) }
42	40, 41	elrab2 3366	. . . . . . . . . . 11 |- ( z e. O <-> ( z e. J /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
43	42	simprbi 480	. . . . . . . . . 10 |- ( z e. O -> E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) )
44	36, 43	syl6 35	. . . . . . . . 9 |- ( x e. ~P O -> ( z e. x -> E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
45	44	ralrimiv 2965	. . . . . . . 8 |- ( x e. ~P O -> A. z e. x E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) )
46		eleq2 2690	. . . . . . . . . 10 |- ( w = ( f ` z ) -> ( A e. w <-> A e. ( f ` z ) ) )
47		fveq2 6191	. . . . . . . . . . 11 |- ( w = ( f ` z ) -> ( ( cls ` J ) ` w ) = ( ( cls ` J ) ` ( f ` z ) ) )
48	47	sseq1d 3632	. . . . . . . . . 10 |- ( w = ( f ` z ) -> ( ( ( cls ` J ) ` w ) C_ ( X \ z ) <-> ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) )
49	46, 48	anbi12d 747	. . . . . . . . 9 |- ( w = ( f ` z ) -> ( ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) <-> ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
50	49	ac6sfi 8204	. . . . . . . 8 |- ( ( x e. Fin /\ A. z e. x E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
51	34, 45, 50	syl2anr 495	. . . . . . 7 |- ( ( x e. ~P O /\ x e. Fin ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
52	33, 51	sylbi 207	. . . . . 6 |- ( x e. ( ~P O i^i Fin ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
53	52	ad2antlr 763	. . . . 5 |- ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
54	3	ad3antrrr 766	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> J e. Top )
55		frn 6053	. . . . . . . 8 |- ( f : x --> J -> ran f C_ J )
56	55	ad2antrl 764	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ran f C_ J )
57		simprr 796	. . . . . . . 8 |- ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> x =/= (/) )
58		simpl 473	. . . . . . . 8 |- ( ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) -> f : x --> J )
59		dm0rn0 5342	. . . . . . . . . . 11 |- ( dom f = (/) <-> ran f = (/) )
60		fdm 6051	. . . . . . . . . . . 12 |- ( f : x --> J -> dom f = x )
61	60	eqeq1d 2624	. . . . . . . . . . 11 |- ( f : x --> J -> ( dom f = (/) <-> x = (/) ) )
62	59, 61	syl5rbbr 275	. . . . . . . . . 10 |- ( f : x --> J -> ( x = (/) <-> ran f = (/) ) )
63	62	necon3bid 2838	. . . . . . . . 9 |- ( f : x --> J -> ( x =/= (/) <-> ran f =/= (/) ) )
64	63	biimpac 503	. . . . . . . 8 |- ( ( x =/= (/) /\ f : x --> J ) -> ran f =/= (/) )
65	57, 58, 64	syl2an 494	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ran f =/= (/) )
66	33	simprbi 480	. . . . . . . . 9 |- ( x e. ( ~P O i^i Fin ) -> x e. Fin )
67	66	ad2antlr 763	. . . . . . . 8 |- ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> x e. Fin )
68		ffn 6045	. . . . . . . . . 10 |- ( f : x --> J -> f Fn x )
69		dffn4 6121	. . . . . . . . . 10 |- ( f Fn x <-> f : x -onto-> ran f )
70	68, 69	sylib 208	. . . . . . . . 9 |- ( f : x --> J -> f : x -onto-> ran f )
71	70	adantr 481	. . . . . . . 8 |- ( ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) -> f : x -onto-> ran f )
72		fofi 8252	. . . . . . . 8 |- ( ( x e. Fin /\ f : x -onto-> ran f ) -> ran f e. Fin )
73	67, 71, 72	syl2an 494	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ran f e. Fin )
74		fiinopn 20706	. . . . . . . 8 |- ( J e. Top -> ( ( ran f C_ J /\ ran f =/= (/) /\ ran f e. Fin ) -> |^| ran f e. J ) )
75	74	imp 445	. . . . . . 7 |- ( ( J e. Top /\ ( ran f C_ J /\ ran f =/= (/) /\ ran f e. Fin ) ) -> |^| ran f e. J )
76	54, 56, 65, 73, 75	syl13anc 1328	. . . . . 6 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^| ran f e. J )
77		simpl 473	. . . . . . . . . 10 |- ( ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> A e. ( f ` z ) )
78	77	ralimi 2952	. . . . . . . . 9 |- ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> A. z e. x A e. ( f ` z ) )
79	78	ad2antll 765	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A. z e. x A e. ( f ` z ) )
80	8	ad3antrrr 766	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A e. ( X \ S ) )
81		eliin 4525	. . . . . . . . 9 |- ( A e. ( X \ S ) -> ( A e. |^|_ z e. x ( f ` z ) <-> A. z e. x A e. ( f ` z ) ) )
82	80, 81	syl 17	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( A e. |^|_ z e. x ( f ` z ) <-> A. z e. x A e. ( f ` z ) ) )
83	79, 82	mpbird 247	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A e. |^|_ z e. x ( f ` z ) )
84	68	ad2antrl 764	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> f Fn x )
85		fnrnfv 6242	. . . . . . . . . 10 |- ( f Fn x -> ran f = { y | E. z e. x y = ( f ` z ) } )
86	85	inteqd 4480	. . . . . . . . 9 |- ( f Fn x -> |^| ran f = |^| { y | E. z e. x y = ( f ` z ) } )
87		fvex 6201	. . . . . . . . . 10 |- ( f ` z ) e. _V
88	87	dfiin2 4555	. . . . . . . . 9 |- |^|_ z e. x ( f ` z ) = |^| { y | E. z e. x y = ( f ` z ) }
89	86, 88	syl6eqr 2674	. . . . . . . 8 |- ( f Fn x -> |^| ran f = |^|_ z e. x ( f ` z ) )
90	84, 89	syl 17	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^| ran f = |^|_ z e. x ( f ` z ) )
91	83, 90	eleqtrrd 2704	. . . . . 6 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A e. |^| ran f )
92	57	adantr 481	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> x =/= (/) )
93	3	ad4antr 768	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> J e. Top )
94		ffvelrn 6357	. . . . . . . . . . . . . . 15 |- ( ( f : x --> J /\ z e. x ) -> ( f ` z ) e. J )
95	94	adantll 750	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) e. J )
96		elssuni 4467	. . . . . . . . . . . . . 14 |- ( ( f ` z ) e. J -> ( f ` z ) C_ U. J )
97	95, 96	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) C_ U. J )
98	97, 5	syl6sseqr 3652	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) C_ X )
99	5	clscld 20851	. . . . . . . . . . . 12 |- ( ( J e. Top /\ ( f ` z ) C_ X ) -> ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
100	93, 98, 99	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
101	100	ralrimiva 2966	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) -> A. z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
102	101	adantrr 753	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A. z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
103		iincld 20843	. . . . . . . . 9 |- ( ( x =/= (/) /\ A. z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
104	92, 102, 103	syl2anc 693	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
105	5	sscls 20860	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ ( f ` z ) C_ X ) -> ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) )
106	93, 98, 105	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) )
107	106	ralrimiva 2966	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) -> A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) )
108		ssel 3597	. . . . . . . . . . . . . 14 |- ( ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> ( y e. ( f ` z ) -> y e. ( ( cls ` J ) ` ( f ` z ) ) ) )
109	108	ral2imi 2947	. . . . . . . . . . . . 13 |- ( A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> ( A. z e. x y e. ( f ` z ) -> A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) ) )
110		vex 3203	. . . . . . . . . . . . . 14 |- y e. _V
111		eliin 4525	. . . . . . . . . . . . . 14 |- ( y e. _V -> ( y e. |^|_ z e. x ( f ` z ) <-> A. z e. x y e. ( f ` z ) ) )
112	110, 111	ax-mp 5	. . . . . . . . . . . . 13 |- ( y e. |^|_ z e. x ( f ` z ) <-> A. z e. x y e. ( f ` z ) )
113		eliin 4525	. . . . . . . . . . . . . 14 |- ( y e. _V -> ( y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) <-> A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) ) )
114	110, 113	ax-mp 5	. . . . . . . . . . . . 13 |- ( y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) <-> A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) )
115	109, 112, 114	3imtr4g 285	. . . . . . . . . . . 12 |- ( A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> ( y e. |^|_ z e. x ( f ` z ) -> y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) ) )
116	115	ssrdv 3609	. . . . . . . . . . 11 |- ( A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> |^|_ z e. x ( f ` z ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
117	107, 116	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) -> |^|_ z e. x ( f ` z ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
118	117	adantrr 753	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( f ` z ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
119	90, 118	eqsstrd 3639	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^| ran f C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
120	5	clsss2 20876	. . . . . . . 8 |- ( ( |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) /\ |^| ran f C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) ) -> ( ( cls ` J ) ` |^| ran f ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
121	104, 119, 120	syl2anc 693	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( ( cls ` J ) ` |^| ran f ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
122		ssel 3597	. . . . . . . . . . . . 13 |- ( ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) -> ( y e. ( ( cls ` J ) ` ( f ` z ) ) -> y e. ( X \ z ) ) )
123	122	adantl 482	. . . . . . . . . . . 12 |- ( ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> ( y e. ( ( cls ` J ) ` ( f ` z ) ) -> y e. ( X \ z ) ) )
124	123	ral2imi 2947	. . . . . . . . . . 11 |- ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> ( A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) -> A. z e. x y e. ( X \ z ) ) )
125		eliin 4525	. . . . . . . . . . . 12 |- ( y e. _V -> ( y e. |^|_ z e. x ( X \ z ) <-> A. z e. x y e. ( X \ z ) ) )
126	110, 125	ax-mp 5	. . . . . . . . . . 11 |- ( y e. |^|_ z e. x ( X \ z ) <-> A. z e. x y e. ( X \ z ) )
127	124, 114, 126	3imtr4g 285	. . . . . . . . . 10 |- ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> ( y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) -> y e. |^|_ z e. x ( X \ z ) ) )
128	127	ssrdv 3609	. . . . . . . . 9 |- ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) C_ |^|_ z e. x ( X \ z ) )
129	128	ad2antll 765	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) C_ |^|_ z e. x ( X \ z ) )
130		iindif2 4589	. . . . . . . . . 10 |- ( x =/= (/) -> |^|_ z e. x ( X \ z ) = ( X \ U_ z e. x z ) )
131	92, 130	syl 17	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( X \ z ) = ( X \ U_ z e. x z ) )
132		simplrl 800	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> S C_ U. x )
133		uniiun 4573	. . . . . . . . . . . 12 |- U. x = U_ z e. x z
134	133	sseq2i 3630	. . . . . . . . . . 11 |- ( S C_ U. x <-> S C_ U_ z e. x z )
135		sscon 3744	. . . . . . . . . . 11 |- ( S C_ U_ z e. x z -> ( X \ U_ z e. x z ) C_ ( X \ S ) )
136	134, 135	sylbi 207	. . . . . . . . . 10 |- ( S C_ U. x -> ( X \ U_ z e. x z ) C_ ( X \ S ) )
137	132, 136	syl 17	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( X \ U_ z e. x z ) C_ ( X \ S ) )
138	131, 137	eqsstrd 3639	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( X \ z ) C_ ( X \ S ) )
139	129, 138	sstrd 3613	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ S ) )
140	121, 139	sstrd 3613	. . . . . 6 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) )
141		eleq2 2690	. . . . . . . 8 |- ( z = |^| ran f -> ( A e. z <-> A e. |^| ran f ) )
142		fveq2 6191	. . . . . . . . 9 |- ( z = |^| ran f -> ( ( cls ` J ) ` z ) = ( ( cls ` J ) ` |^| ran f ) )
143	142	sseq1d 3632	. . . . . . . 8 |- ( z = |^| ran f -> ( ( ( cls ` J ) ` z ) C_ ( X \ S ) <-> ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) ) )
144	141, 143	anbi12d 747	. . . . . . 7 |- ( z = |^| ran f -> ( ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) <-> ( A e. |^| ran f /\ ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) ) ) )
145	144	rspcev 3309	. . . . . 6 |- ( ( |^| ran f e. J /\ ( A e. |^| ran f /\ ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
146	76, 91, 140, 145	syl12anc 1324	. . . . 5 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
147	53, 146	exlimddv 1863	. . . 4 |- ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
148	147	anassrs 680	. . 3 |- ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x =/= (/) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
149	32, 148	pm2.61dane 2881	. 2 |- ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
150	1	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> J e. Haus )
151		hauscmplem.4	. . . . . . . . 9 |- ( ph -> S C_ X )
152	151	sselda 3603	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> x e. X )
153	9	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> A e. X )
154		id 22	. . . . . . . . 9 |- ( x e. S -> x e. S )
155	8	eldifbd 3587	. . . . . . . . 9 |- ( ph -> -. A e. S )
156		nelne2 2891	. . . . . . . . 9 |- ( ( x e. S /\ -. A e. S ) -> x =/= A )
157	154, 155, 156	syl2anr 495	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> x =/= A )
158	5	hausnei 21132	. . . . . . . 8 |- ( ( J e. Haus /\ ( x e. X /\ A e. X /\ x =/= A ) ) -> E. y e. J E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) )
159	150, 152, 153, 157, 158	syl13anc 1328	. . . . . . 7 |- ( ( ph /\ x e. S ) -> E. y e. J E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) )
160		3anass 1042	. . . . . . . . . . 11 |- ( ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) <-> ( x e. y /\ ( A e. w /\ ( y i^i w ) = (/) ) ) )
161		elssuni 4467	. . . . . . . . . . . . . . . . 17 |- ( w e. J -> w C_ U. J )
162	161, 5	syl6sseqr 3652	. . . . . . . . . . . . . . . 16 |- ( w e. J -> w C_ X )
163	162	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> w C_ X )
164		incom 3805	. . . . . . . . . . . . . . . . 17 |- ( y i^i w ) = ( w i^i y )
165	164	eqeq1i 2627	. . . . . . . . . . . . . . . 16 |- ( ( y i^i w ) = (/) <-> ( w i^i y ) = (/) )
166		reldisj 4020	. . . . . . . . . . . . . . . 16 |- ( w C_ X -> ( ( w i^i y ) = (/) <-> w C_ ( X \ y ) ) )
167	165, 166	syl5bb 272	. . . . . . . . . . . . . . 15 |- ( w C_ X -> ( ( y i^i w ) = (/) <-> w C_ ( X \ y ) ) )
168	163, 167	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( y i^i w ) = (/) <-> w C_ ( X \ y ) ) )
169	150, 2	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. S ) -> J e. Top )
170	5	opncld 20837	. . . . . . . . . . . . . . . . 17 |- ( ( J e. Top /\ y e. J ) -> ( X \ y ) e. ( Clsd ` J ) )
171	169, 170	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. S ) /\ y e. J ) -> ( X \ y ) e. ( Clsd ` J ) )
172	171	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( X \ y ) e. ( Clsd ` J ) )
173	5	clsss2 20876	. . . . . . . . . . . . . . . 16 |- ( ( ( X \ y ) e. ( Clsd ` J ) /\ w C_ ( X \ y ) ) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) )
174	173	ex 450	. . . . . . . . . . . . . . 15 |- ( ( X \ y ) e. ( Clsd ` J ) -> ( w C_ ( X \ y ) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) ) )
175	172, 174	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( w C_ ( X \ y ) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) ) )
176	168, 175	sylbid 230	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( y i^i w ) = (/) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) ) )
177	176	anim2d 589	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( A e. w /\ ( y i^i w ) = (/) ) -> ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
178	177	anim2d 589	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( x e. y /\ ( A e. w /\ ( y i^i w ) = (/) ) ) -> ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
179	160, 178	syl5bi 232	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
180	179	reximdva 3017	. . . . . . . . 9 |- ( ( ( ph /\ x e. S ) /\ y e. J ) -> ( E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> E. w e. J ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
181		r19.42v 3092	. . . . . . . . 9 |- ( E. w e. J ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) <-> ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
182	180, 181	syl6ib 241	. . . . . . . 8 |- ( ( ( ph /\ x e. S ) /\ y e. J ) -> ( E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
183	182	reximdva 3017	. . . . . . 7 |- ( ( ph /\ x e. S ) -> ( E. y e. J E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
184	159, 183	mpd 15	. . . . . 6 |- ( ( ph /\ x e. S ) -> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
185	41	unieqi 4445	. . . . . . . 8 |- U. O = U. { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) }
186	185	eleq2i 2693	. . . . . . 7 |- ( x e. U. O <-> x e. U. { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) } )
187		elunirab 4448	. . . . . . 7 |- ( x e. U. { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) } <-> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
188	186, 187	bitri 264	. . . . . 6 |- ( x e. U. O <-> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
189	184, 188	sylibr 224	. . . . 5 |- ( ( ph /\ x e. S ) -> x e. U. O )
190	189	ex 450	. . . 4 |- ( ph -> ( x e. S -> x e. U. O ) )
191	190	ssrdv 3609	. . 3 |- ( ph -> S C_ U. O )
192		ssrab2 3687	. . . . . 6 |- { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) } C_ J
193	41, 192	eqsstri 3635	. . . . 5 |- O C_ J
194		elpw2g 4827	. . . . . 6 |- ( J e. Haus -> ( O e. ~P J <-> O C_ J ) )
195	1, 194	syl 17	. . . . 5 |- ( ph -> ( O e. ~P J <-> O C_ J ) )
196	193, 195	mpbiri 248	. . . 4 |- ( ph -> O e. ~P J )
197		hauscmplem.5	. . . . 5 |- ( ph -> ( J ↾t S ) e. Comp )
198	5	cmpsub 21203	. . . . . 6 |- ( ( J e. Top /\ S C_ X ) -> ( ( J ↾t S ) e. Comp <-> A. z e. ~P J ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) ) )
199	198	biimp3a 1432	. . . . 5 |- ( ( J e. Top /\ S C_ X /\ ( J ↾t S ) e. Comp ) -> A. z e. ~P J ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) )
200	3, 151, 197, 199	syl3anc 1326	. . . 4 |- ( ph -> A. z e. ~P J ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) )
201		unieq 4444	. . . . . . 7 |- ( z = O -> U. z = U. O )
202	201	sseq2d 3633	. . . . . 6 |- ( z = O -> ( S C_ U. z <-> S C_ U. O ) )
203		pweq 4161	. . . . . . . 8 |- ( z = O -> ~P z = ~P O )
204	203	ineq1d 3813	. . . . . . 7 |- ( z = O -> ( ~P z i^i Fin ) = ( ~P O i^i Fin ) )
205	204	rexeqdv 3145	. . . . . 6 |- ( z = O -> ( E. x e. ( ~P z i^i Fin ) S C_ U. x <-> E. x e. ( ~P O i^i Fin ) S C_ U. x ) )
206	202, 205	imbi12d 334	. . . . 5 |- ( z = O -> ( ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) <-> ( S C_ U. O -> E. x e. ( ~P O i^i Fin ) S C_ U. x ) ) )
207	206	rspcva 3307	. . . 4 |- ( ( O e. ~P J /\ A. z e. ~P J ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) ) -> ( S C_ U. O -> E. x e. ( ~P O i^i Fin ) S C_ U. x ) )
208	196, 200, 207	syl2anc 693	. . 3 |- ( ph -> ( S C_ U. O -> E. x e. ( ~P O i^i Fin ) S C_ U. x ) )
209	191, 208	mpd 15	. 2 |- ( ph -> E. x e. ( ~P O i^i Fin ) S C_ U. x )
210	149, 209	r19.29a 3078	1 |- ( ph -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   |^|cint 4475   U_ciun 4520   |^|_ciin 4521   dom cdm 5114   ran crn 5115   Fn wfn 5883   -->wf 5884   -onto->wfo 5886   ` cfv 5888  (class class class)co 6650   Fincfn 7955   ↾_t crest 16081   Topctop 20698   Clsdccld 20820   clsccl 20822   Hauscha 21112   Compccmp 21189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-cls 20825  df-haus 21119  df-cmp 21190

This theorem is referenced by:  hauscmp  21210  hausllycmp  21297