Theorem fcluscomplem 11732

Description: Lemma for fcluscomp 11733.

Hypothesis

Ref	Expression
fcluscomp.1	|- X = U.J

Assertion

Ref	Expression
fcluscomplem	|- ((J e. Top /\ f e. Fil /\ X = U.f) -> A.x e. (fi` {y | E.s e. f y = ((cls` J)` s)})E.z e. f z (_ x)

Distinct variable groups:   f,s,x,y,z,J   f,X,s,x,y,z

Proof of Theorem fcluscomplem

Step	Hyp	Ref	Expression
1		abrexexg 3975	. . . . 5 |- (f e. Fil -> {y | E.s e. f y = ((cls` J)` s)} e. V)
2		visset 1859	. . . . . 6 |- x e. V
3		sppfi 10851	. . . . . 6 |- ((x e. V /\ {y | E.s e. f y = ((cls` J)` s)} e. V) -> (x e. (fi` {y | E.s e. f y = ((cls` J)` s)}) <-> E.w(w (_ {y | E.s e. f y = ((cls` J)` s)} /\ w e. Fin /\ x = |^|w)))
4	2, 3	mpan 699	. . . . 5 |- ({y | E.s e. f y = ((cls` J)` s)} e. V -> (x e. (fi` {y | E.s e. f y = ((cls` J)` s)}) <-> E.w(w (_ {y | E.s e. f y = ((cls` J)` s)} /\ w e. Fin /\ x = |^|w)))
5	1, 4	syl 10	. . . 4 |- (f e. Fil -> (x e. (fi` {y | E.s e. f y = ((cls` J)` s)}) <-> E.w(w (_ {y | E.s e. f y = ((cls` J)` s)} /\ w e. Fin /\ x = |^|w)))
6	5	3ad2ant2 807	. . 3 |- ((J e. Top /\ f e. Fil /\ X = U.f) -> (x e. (fi` {y | E.s e. f y = ((cls` J)` s)}) <-> E.w(w (_ {y | E.s e. f y = ((cls` J)` s)} /\ w e. Fin /\ x = |^|w)))
7		sseq2 2135	. . . . . . . 8 |- (x = |^|w -> (z (_ x <-> z (_ |^|w))
8	7	rexbidv 1710	. . . . . . 7 |- (x = |^|w -> (E.z e. f z (_ x <-> E.z e. f z (_ |^|w))
9		breq2 2696	. . . . . . . . . . . . . . . 16 |- (k = (/) -> (w ~~ k <-> w ~~ (/)))
10	9	imbi1d 616	. . . . . . . . . . . . . . 15 |- (k = (/) -> ((w ~~ k -> E.z e. f z (_ |^|w) <-> (w ~~ (/) -> E.z e. f z (_ |^|w)))
11	10	imbi2d 615	. . . . . . . . . . . . . 14 |- (k = (/) -> ((((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ (/) -> E.z e. f z (_ |^|w))))
12	11	albidv 1316	. . . . . . . . . . . . 13 |- (k = (/) -> (A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ (/) -> E.z e. f z (_ |^|w))))
13		breq2 2696	. . . . . . . . . . . . . . . 16 |- (k = j -> (w ~~ k <-> w ~~ j))
14	13	imbi1d 616	. . . . . . . . . . . . . . 15 |- (k = j -> ((w ~~ k -> E.z e. f z (_ |^|w) <-> (w ~~ j -> E.z e. f z (_ |^|w)))
15	14	imbi2d 615	. . . . . . . . . . . . . 14 |- (k = j -> ((((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ j -> E.z e. f z (_ |^|w))))
16	15	albidv 1316	. . . . . . . . . . . . 13 |- (k = j -> (A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ j -> E.z e. f z (_ |^|w))))
17		breq2 2696	. . . . . . . . . . . . . . . 16 |- (k = suc j -> (w ~~ k <-> w ~~ suc j))
18	17	imbi1d 616	. . . . . . . . . . . . . . 15 |- (k = suc j -> ((w ~~ k -> E.z e. f z (_ |^|w) <-> (w ~~ suc j -> E.z e. f z (_ |^|w)))
19	18	imbi2d 615	. . . . . . . . . . . . . 14 |- (k = suc j -> ((((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ suc j -> E.z e. f z (_ |^|w))))
20	19	albidv 1316	. . . . . . . . . . . . 13 |- (k = suc j -> (A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ suc j -> E.z e. f z (_ |^|w))))
21		breq2 2696	. . . . . . . . . . . . . . . 16 |- (k = n -> (w ~~ k <-> w ~~ n))
22	21	imbi1d 616	. . . . . . . . . . . . . . 15 |- (k = n -> ((w ~~ k -> E.z e. f z (_ |^|w) <-> (w ~~ n -> E.z e. f z (_ |^|w)))
23	22	imbi2d 615	. . . . . . . . . . . . . 14 |- (k = n -> ((((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ n -> E.z e. f z (_ |^|w))))
24	23	albidv 1316	. . . . . . . . . . . . 13 |- (k = n -> (A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ k -> E.z e. f z (_ |^|w)) <-> A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ n -> E.z e. f z (_ |^|w))))
25		inteq 2603	. . . . . . . . . . . . . . . . . . . 20 |- (w = (/) -> |^|w = |^|(/))
26	25	sseq2d 2141	. . . . . . . . . . . . . . . . . . 19 |- (w = (/) -> (z (_ |^|w <-> z (_ |^|(/)))
27	26	rexbidv 1710	. . . . . . . . . . . . . . . . . 18 |- (w = (/) -> (E.z e. f z (_ |^|w <-> E.z e. f z (_ |^|(/)))
28		eqid 1518	. . . . . . . . . . . . . . . . . . . 20 |- U.f = U.f
29	28	filusb 11074	. . . . . . . . . . . . . . . . . . 19 |- (f e. Fil -> U.f e. f)
30		ssv 2133	. . . . . . . . . . . . . . . . . . . . 21 |- U.f (_ V
31		int0 2614	. . . . . . . . . . . . . . . . . . . . 21 |- |^|(/) = V
32	30, 31	sseqtr4i 2146	. . . . . . . . . . . . . . . . . . . 20 |- U.f (_ |^|(/)
33		sseq1 2134	. . . . . . . . . . . . . . . . . . . . 21 |- (z = U.f -> (z (_ |^|(/) <-> U.f (_ |^|(/)))
34	33	rcla4ev 1923	. . . . . . . . . . . . . . . . . . . 20 |- ((U.f e. f /\ U.f (_ |^|(/)) -> E.z e. f z (_ |^|(/))
35	32, 34	mpan2 700	. . . . . . . . . . . . . . . . . . 19 |- (U.f e. f -> E.z e. f z (_ |^|(/))
36	29, 35	syl 10	. . . . . . . . . . . . . . . . . 18 |- (f e. Fil -> E.z e. f z (_ |^|(/))
37	27, 36	syl5cbir 209	. . . . . . . . . . . . . . . . 17 |- (f e. Fil -> (w = (/) -> E.z e. f z (_ |^|w))
38	37	3ad2ant2 807	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ f e. Fil /\ X = U.f) -> (w = (/) -> E.z e. f z (_ |^|w))
39	38	adantr 389	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w = (/) -> E.z e. f z (_ |^|w))
40		en0 4564	. . . . . . . . . . . . . . 15 |- (w ~~ (/) <-> w = (/))
41	39, 40	syl5ib 204	. . . . . . . . . . . . . 14 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ (/) -> E.z e. f z (_ |^|w))
42	41	ax-gen 999	. . . . . . . . . . . . 13 |- A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ (/) -> E.z e. f z (_ |^|w))
43		visset 1859	. . . . . . . . . . . . . . . . . . . 20 |- j e. V
44	43	sucex 3168	. . . . . . . . . . . . . . . . . . 19 |- suc j e. V
45	44	bren 4518	. . . . . . . . . . . . . . . . . 18 |- (w ~~ suc j <-> E.g g:w-1-1-onto->suc j)
46		f1ocnv 3809	. . . . . . . . . . . . . . . . . . . 20 |- (g:w-1-1-onto->suc j -> `'g:suc j-1-1-onto->w)
47		f1of1 3796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (`'g:suc j-1-1-onto->w -> `'g:suc j-1-1->w)
48		sssucid 3050	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- j (_ suc j
49		f1ores 3811	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((`'g:suc j-1-1->w /\ j (_ suc j) -> (`'g |` j):j-1-1-onto->(`'g"j))
50	48, 49	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (`'g:suc j-1-1->w -> (`'g |` j):j-1-1-onto->(`'g"j))
51	47, 50	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (`'g:suc j-1-1-onto->w -> (`'g |` j):j-1-1-onto->(`'g"j))
52	51	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (`'g |` j):j-1-1-onto->(`'g"j))
53	43	f1oen 4539	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((`'g |` j):j-1-1-onto->(`'g"j) -> j ~~ (`'g"j))
54		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- g e. V
55	54	cnvex 3625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- `'g e. V
56		imaexg 3508	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (`'g e. V -> (`'g"j) e. V)
57	55, 56	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (`'g"j) e. V
58	57	ensym 4553	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j ~~ (`'g"j) -> (`'g"j) ~~ j)
59	52, 53, 58	3syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (`'g"j) ~~ j)
60		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = (`'g"j) -> (x (_ {y | E.s e. f y = ((cls` J)` s)} <-> (`'g"j) (_ {y | E.s e. f y = ((cls` J)` s)}))
61	60	anbi2d 619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = (`'g"j) -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) <-> ((J e. Top /\ f e. Fil /\ X = U.f) /\ (`'g"j) (_ {y | E.s e. f y = ((cls` J)` s)})))
62		breq1 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = (`'g"j) -> (x ~~ j <-> (`'g"j) ~~ j))
63		inteq 2603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = (`'g"j) -> |^|x = |^|(`'g"j))
64	63	sseq2d 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = (`'g"j) -> (z (_ |^|x <-> z (_ |^|(`'g"j)))
65	64	rexbidv 1710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = (`'g"j) -> (E.z e. f z (_ |^|x <-> E.z e. f z (_ |^|(`'g"j)))
66	62, 65	imbi12d 629	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = (`'g"j) -> ((x ~~ j -> E.z e. f z (_ |^|x) <-> ((`'g"j) ~~ j -> E.z e. f z (_ |^|(`'g"j))))
67	61, 66	imbi12d 629	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = (`'g"j) -> ((((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) <-> (((J e. Top /\ f e. Fil /\ X = U.f) /\ (`'g"j) (_ {y | E.s e. f y = ((cls` J)` s)}) -> ((`'g"j) ~~ j -> E.z e. f z (_ |^|(`'g"j)))))
68	57, 67	cla4v 1914	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ (`'g"j) (_ {y | E.s e. f y = ((cls` J)` s)}) -> ((`'g"j) ~~ j -> E.z e. f z (_ |^|(`'g"j))))
69		simprl 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (J e. Top /\ f e. Fil /\ X = U.f))
70		f1ofo 3803	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (`'g:suc j-1-1-onto->w -> `'g:suc j-onto->w)
71		forn 3782	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (`'g:suc j-onto->w -> ran `' g = w)
72		imassrn 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (`'g"j) (_ ran `' g
73		sseq2 2135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (ran `' g = w -> ((`'g"j) (_ ran `' g <-> (`'g"j) (_ w))
74	72, 73	mpbii 191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (ran `' g = w -> (`'g"j) (_ w)
75	70, 71, 74	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (`'g:suc j-1-1-onto->w -> (`'g"j) (_ w)
76	75	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (`'g"j) (_ w)
77		simprr 415	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> w (_ {y | E.s e. f y = ((cls` J)` s)})
78	76, 77	sstrd 2126	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (`'g"j) (_ {y | E.s e. f y = ((cls` J)` s)})
79	69, 78	jca 286	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> ((J e. Top /\ f e. Fil /\ X = U.f) /\ (`'g"j) (_ {y | E.s e. f y = ((cls` J)` s)}))
80	68, 79	syl5com 52	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> ((`'g"j) ~~ j -> E.z e. f z (_ |^|(`'g"j))))
81	59, 80	mpid 47	. . . . . . . . . . . . . . . . . . . . . 22 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> E.z e. f z (_ |^|(`'g"j)))
82		ssel 2115	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w (_ {y | E.s e. f y = ((cls` J)` s)} -> ((`'g` j) e. w -> (`'g` j) e. {y | E.s e. f y = ((cls` J)` s)}))
83		f1of 3797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (`'g:suc j-1-1-onto->w -> `'g:suc j-->w)
84	43	sucid 3051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- j e. suc j
85		ffvelrn 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((`'g:suc j-->w /\ j e. suc j) -> (`'g` j) e. w)
86	84, 85	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (`'g:suc j-->w -> (`'g` j) e. w)
87	83, 86	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (`'g:suc j-1-1-onto->w -> (`'g` j) e. w)
88	82, 87	syl5com 52	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (`'g:suc j-1-1-onto->w -> (w (_ {y | E.s e. f y = ((cls` J)` s)} -> (`'g` j) e. {y | E.s e. f y = ((cls` J)` s)}))
89	88	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> (w (_ {y | E.s e. f y = ((cls` J)` s)} -> (`'g` j) e. {y | E.s e. f y = ((cls` J)` s)}))
90		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z = (x i^i s) -> (z (_ |^|w <-> (x i^i s) (_ |^|w))
91	90	rcla4ev 1923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((x i^i s) e. f /\ (x i^i s) (_ |^|w) -> E.z e. f z (_ |^|w)
92		filint 11075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((f e. Fil /\ x e. f /\ s e. f) -> (x i^i s) e. f)
93	92	3com23 845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((f e. Fil /\ s e. f /\ x e. f) -> (x i^i s) e. f)
94	93	3expb 840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f e. Fil /\ (s e. f /\ x e. f)) -> (x i^i s) e. f)
95	94	3ad2antl2 816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ (s e. f /\ x e. f)) -> (x i^i s) e. f)
96	95	anassrs 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((J e. Top /\ f e. Fil /\ X = U.f) /\ s e. f) /\ x e. f) -> (x i^i s) e. f)
97	96	adantrl 394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((J e. Top /\ f e. Fil /\ X = U.f) /\ s e. f) /\ ((`'g` j) = ((cls` J)` s) /\ x e. f)) -> (x i^i s) e. f)
98	97	adantlll 396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ ((`'g` j) = ((cls` J)` s) /\ x e. f)) -> (x i^i s) e. f)
99	98	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (x i^i s) e. f)
100		ss2in 2288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((x (_ |^|(`'g"j) /\ s (_ (`'g` j)) -> (x i^i s) (_ (|^|(`'g"j) i^i (`'g` j)))
101		simprr 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> x (_ |^|(`'g"j))
102		fcluscomp.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- X = U.J
103	102	sscls 7899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((J e. Top /\ s (_ X) -> s (_ ((cls` J)` s))
104		3simpr1 11379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> J e. Top)
105	104	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> J e. Top)
106		elssuni 2593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (s e. f -> s (_ U.f)
107	106	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((X = U.f /\ s e. f) -> s (_ U.f)
108		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((X = U.f /\ s e. f) -> X = U.f)
109	107, 108	sseqtr4d 2150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((X = U.f /\ s e. f) -> s (_ X)
110	109	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ s e. f) -> s (_ X)
111	110	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) -> s (_ X)
112	111	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> s (_ X)
113	103, 105, 112	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> s (_ ((cls` J)` s))
114		simprll 11366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (`'g` j) = ((cls` J)` s))
115	113, 114	sseqtr4d 2150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> s (_ (`'g` j))
116	100, 101, 115	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (x i^i s) (_ (|^|(`'g"j) i^i (`'g` j)))
117		fnsnfv 3878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((`'g Fn suc j /\ j e. suc j) -> {(`'g` j)} = (`'g"{j}))
118		f1ofn 3798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (`'g:suc j-1-1-onto->w -> `'g Fn suc j)
119	118	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> `'g Fn suc j)
120	119	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> `'g Fn suc j)
121	84	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> j e. suc j)
122	117, 120, 121	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> {(`'g` j)} = (`'g"{j}))
123	122	inteqd 2605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> |^|{(`'g` j)} = |^|(`'g"{j}))
124		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'g` j) e. V
125	124	intsn 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- |^|{(`'g` j)} = (`'g` j)
126	123, 125	syl5eqr 1564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (`'g` j) = |^|(`'g"{j}))
127	126	ineq2d 2269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (|^|(`'g"j) i^i (`'g` j)) = (|^|(`'g"j) i^i |^|(`'g"{j})))
128		intun 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- |^|((`'g"j) u. (`'g"{j})) = (|^|(`'g"j) i^i |^|(`'g"{j}))
129	127, 128	syl6eqr 1568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (|^|(`'g"j) i^i (`'g` j)) = |^|((`'g"j) u. (`'g"{j})))
130		foima 3784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (`'g:suc j-onto->w -> (`'g"suc j) = w)
131	70, 130	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'g:suc j-1-1-onto->w -> (`'g"suc j) = w)
132	131	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> (`'g"suc j) = w)
133	132	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (`'g"suc j) = w)
134		df-suc 2981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- suc j = (j u. {j})
135	134	imaeq2i 3494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'g"suc j) = (`'g"(j u. {j}))
136		imaundi 3545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'g"(j u. {j})) = ((`'g"j) u. (`'g"{j}))
137	135, 136	eqtr2i 1539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((`'g"j) u. (`'g"{j})) = (`'g"suc j)
138	133, 137	syl5eq 1562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> ((`'g"j) u. (`'g"{j})) = w)
139	138	inteqd 2605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> |^|((`'g"j) u. (`'g"{j})) = |^|w)
140	129, 139	eqtrd 1550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (|^|(`'g"j) i^i (`'g` j)) = |^|w)
141	116, 140	sseqtrd 2149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> (x i^i s) (_ |^|w)
142	91, 99, 141	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) /\ s e. f) /\ (((`'g` j) = ((cls` J)` s) /\ x e. f) /\ x (_ |^|(`'g"j))) -> E.z e. f z (_ |^|w)
143	142	exp58 11355	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> (s e. f -> ((`'g` j) = ((cls` J)` s) -> (x e. f -> (x (_ |^|(`'g"j) -> E.z e. f z (_ |^|w)))))
144	143	r19.23adv 1792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> (E.s e. f (`'g` j) = ((cls` J)` s) -> (x e. f -> (x (_ |^|(`'g"j) -> E.z e. f z (_ |^|w))))
145		eqeq1 1524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = (`'g` j) -> (y = ((cls` J)` s) <-> (`'g` j) = ((cls` J)` s)))
146	145	rexbidv 1710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = (`'g` j) -> (E.s e. f y = ((cls` J)` s) <-> E.s e. f (`'g` j) = ((cls` J)` s)))
147	124, 146	elab 1943	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((`'g` j) e. {y | E.s e. f y = ((cls` J)` s)} <-> E.s e. f (`'g` j) = ((cls` J)` s))
148	144, 147	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> ((`'g` j) e. {y | E.s e. f y = ((cls` J)` s)} -> (x e. f -> (x (_ |^|(`'g"j) -> E.z e. f z (_ |^|w))))
149	89, 148	syld 27	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((`'g:suc j-1-1-onto->w /\ (J e. Top /\ f e. Fil /\ X = U.f)) -> (w (_ {y | E.s e. f y = ((cls` J)` s)} -> (x e. f -> (x (_ |^|(`'g"j) -> E.z e. f z (_ |^|w))))
150	149	impr 11359	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (x e. f -> (x (_ |^|(`'g"j) -> E.z e. f z (_ |^|w)))
151	150	r19.23adv 1792	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (E.x e. f x (_ |^|(`'g"j) -> E.z e. f z (_ |^|w))
152		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = x -> (z (_ |^|(`'g"j) <-> x (_ |^|(`'g"j)))
153	152	cbvrexv 1847	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.z e. f z (_ |^|(`'g"j) <-> E.x e. f x (_ |^|(`'g"j))
154	151, 153	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . 22 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (E.z e. f z (_ |^|(`'g"j) -> E.z e. f z (_ |^|w))
155	81, 154	syld 27	. . . . . . . . . . . . . . . . . . . . 21 |- ((`'g:suc j-1-1-onto->w /\ ((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)})) -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> E.z e. f z (_ |^|w))
156	155	ex 371	. . . . . . . . . . . . . . . . . . . 20 |- (`'g:suc j-1-1-onto->w -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> E.z e. f z (_ |^|w)))
157	46, 156	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (g:w-1-1-onto->suc j -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> E.z e. f z (_ |^|w)))
158	157	19.23aiv 1333	. . . . . . . . . . . . . . . . . 18 |- (E.g g:w-1-1-onto->suc j -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> E.z e. f z (_ |^|w)))
159	45, 158	sylbi 197	. . . . . . . . . . . . . . . . 17 |- (w ~~ suc j -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> E.z e. f z (_ |^|w)))
160	159	com13 33	. . . . . . . . . . . . . . . 16 |- (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ suc j -> E.z e. f z (_ |^|w)))
161	160	a1i 8	. . . . . . . . . . . . . . 15 |- (j e. om -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ suc j -> E.z e. f z (_ |^|w))))
162	161	19.21adv 1326	. . . . . . . . . . . . . 14 |- (j e. om -> (A.x(((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)}) -> (x ~~ j -> E.z e. f z (_ |^|x)) -> A.w(((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) -> (w ~~ suc j -> E.z e. f z (_ |^|w))))
163		sseq1 2134	. . . . . . . . . . . . . . . . 17 |- (w = x -> (w (_ {y | E.s e. f y = ((cls` J)` s)} <-> x (_ {y | E.s e. f y = ((cls` J)` s)}))
164	163	anbi2d 619	. . . . . . . . . . . . . . . 16 |- (w = x -> (((J e. Top /\ f e. Fil /\ X = U.f) /\ w (_ {y | E.s e. f y = ((cls` J)` s)}) <-> ((J e. Top /\ f e. Fil /\ X = U.f) /\ x (_ {y | E.s e. f y = ((cls` J)` s)})))
165		breq1 2695	. . . . . . . . . . . . . . . . 17 |- (w = x -> (w ~~ j <-> x ~~ j))
166		inteq 2603	. . . . . . . . . . . . . . . . . . 19 |- (w = x -> |^|w = |^|x)
167	166	sseq2d 2141	. . . . . . . . . . . . . . . . . 18 |- (w = x -> (z (_ |^|w <-> z (_ |^|x))
168	167	rexbidv 1710	. . . . . . . . . . . . . . . . 17 |- (w = x -> (E.z e. f z (_ |^|w <->