Theorem compsublem 15430

Description: Lemma for compsub 15431.

Hypothesis

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

Assertion

Ref	Expression
compsublem	|- ((J e. Top /\ S C_ X) -> (A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d) -> A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))

Distinct variable groups:   c,d,s,t,J   S,c,d,s,t   X,c,d,s,t

Proof of Theorem compsublem

Step	Hyp	Ref	Expression
1		unieq 3185	. . . . . . . 8 |- (c = {y e. J | (y i^i S) e. s} -> U.c = U.{y e. J | (y i^i S) e. s})
2	1	sseq2d 2645	. . . . . . 7 |- (c = {y e. J | (y i^i S) e. s} -> (S C_ U.c <-> S C_ U.{y e. J | (y i^i S) e. s}))
3		pweq 3036	. . . . . . . . 9 |- (c = {y e. J | (y i^i S) e. s} -> ~Pc = ~P{y e. J | (y i^i S) e. s})
4	3	ineq1d 2795	. . . . . . . 8 |- (c = {y e. J | (y i^i S) e. s} -> (~Pc i^i Fin) = (~P{y e. J | (y i^i S) e. s} i^i Fin))
5	4	rexeqdv 2270	. . . . . . 7 |- (c = {y e. J | (y i^i S) e. s} -> (E.d e. (~Pc i^i Fin)S C_ U.d <-> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d))
6	2, 5	imbi12d 688	. . . . . 6 |- (c = {y e. J | (y i^i S) e. s} -> ((S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d) <-> (S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d)))
7	6	rcla4va 2378	. . . . 5 |- (({y e. J | (y i^i S) e. s} e. ~PJ /\ A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)) -> (S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d))
8		rabexg 3460	. . . . . . 7 |- (J e. Top -> {y e. J | (y i^i S) e. s} e. _V)
9	8	ad2antrr 440	. . . . . 6 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> {y e. J | (y i^i S) e. s} e. _V)
10		ssrab2 2692	. . . . . . 7 |- {y e. J | (y i^i S) e. s} C_ J
11		elpwg 3038	. . . . . . 7 |- ({y e. J | (y i^i S) e. s} e. _V -> ({y e. J | (y i^i S) e. s} e. ~PJ <-> {y e. J | (y i^i S) e. s} C_ J))
12	10, 11	mpbiri 211	. . . . . 6 |- ({y e. J | (y i^i S) e. s} e. _V -> {y e. J | (y i^i S) e. s} e. ~PJ)
13	9, 12	syl 12	. . . . 5 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> {y e. J | (y i^i S) e. s} e. ~PJ)
14	7, 13	sylan 497	. . . 4 |- ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)) -> (S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d))
15	14	ex 402	. . 3 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> (A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d) -> (S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d)))
16		stoig2 10252	. . . . . . . 8 |- ((J e. Top /\ S C_ U.J) -> U.(subSp` <.S, J>.) = S)
17		compsub.1	. . . . . . . . 9 |- X = U.J
18	17	sseq2i 2642	. . . . . . . 8 |- (S C_ X <-> S C_ U.J)
19	16, 18	sylan2b 501	. . . . . . 7 |- ((J e. Top /\ S C_ X) -> U.(subSp` <.S, J>.) = S)
20	19	adantr 425	. . . . . 6 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> U.(subSp` <.S, J>.) = S)
21	20	eqeq1d 1892	. . . . 5 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> (U.(subSp` <.S, J>.) = U.s <-> S = U.s))
22		eleq2 1958	. . . . . . . . . . . . . . 15 |- (S = U.s -> (t e. S <-> t e. U.s))
23		eluni 3180	. . . . . . . . . . . . . . 15 |- (t e. U.s <-> E.u(t e. u /\ u e. s))
24	22, 23	syl6bb 595	. . . . . . . . . . . . . 14 |- (S = U.s -> (t e. S <-> E.u(t e. u /\ u e. s)))
25	24	adantl 424	. . . . . . . . . . . . 13 |- ((((J e. Top /\ S C_ X) /\ s C_ (subSp` <.S, J>.)) /\ S = U.s) -> (t e. S <-> E.u(t e. u /\ u e. s)))
26		ssel 2615	. . . . . . . . . . . . . . . . . . 19 |- (s C_ (subSp` <.S, J>.) -> (u e. s -> u e. (subSp` <.S, J>.)))
27		simpl 346	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ S C_ X) -> J e. Top)
28		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- u e. _V
29	28	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ S C_ X) -> u e. _V)
30		ssexg 3457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((S C_ U.J /\ U.J e. _V) -> S e. _V)
31	30	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((U.J e. _V /\ S C_ U.J) -> S e. _V)
32		uniexg 3795	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (J e. Top -> U.J e. _V)
33	31, 32	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ S C_ U.J) -> S e. _V)
34	33, 18	sylan2b 501	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ S C_ X) -> S e. _V)
35		issubspt 10247	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ u e. _V /\ S e. _V) -> (u e. (subSp` <.S, J>.) <-> E.w e. J u = (w i^i S)))
36	27, 29, 34, 35	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- ((J e. Top /\ S C_ X) -> (u e. (subSp` <.S, J>.) <-> E.w e. J u = (w i^i S)))
37		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u C_ w /\ t e. u) -> t e. w)
38		inss1 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w i^i S) C_ w
39		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (u = (w i^i S) -> (u C_ w <-> (w i^i S) C_ w))
40	38, 39	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (u = (w i^i S) -> u C_ w)
41	37, 40	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u = (w i^i S) /\ t e. u) -> t e. w)
42	41	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) /\ t e. u) -> t e. w)
43	42	3adant2 895	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) /\ u e. s /\ t e. u) -> t e. w)
44		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = w -> (y i^i S) = (w i^i S))
45	44	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = w -> ((y i^i S) e. s <-> (w i^i S) e. s))
46	45	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w e. {y e. J | (y i^i S) e. s} <-> (w e. J /\ (w i^i S) e. s))
47		simp2 877	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) -> w e. J)
48	47	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) /\ u e. s /\ t e. u) -> w e. J)
49		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (u = (w i^i S) -> (u e. s <-> (w i^i S) e. s))
50	49	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u = (w i^i S) /\ u e. s) -> (w i^i S) e. s)
51	50	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) /\ u e. s) -> (w i^i S) e. s)
52	51	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) /\ u e. s /\ t e. u) -> (w i^i S) e. s)
53	46, 48, 52	sylanbrc 527	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) /\ u e. s /\ t e. u) -> w e. {y e. J | (y i^i S) e. s})
54		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- w e. _V
55		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v = w -> (t e. v <-> t e. w))
56		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v = w -> (v e. {y e. J | (y i^i S) e. s} <-> w e. {y e. J | (y i^i S) e. s}))
57	55, 56	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v = w -> ((t e. v /\ v e. {y e. J | (y i^i S) e. s}) <-> (t e. w /\ w e. {y e. J | (y i^i S) e. s})))
58	54, 57	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((t e. w /\ w e. {y e. J | (y i^i S) e. s}) -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))
59	43, 53, 58	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) /\ u e. s /\ t e. u) -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))
60	59	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ S C_ X) /\ w e. J /\ u = (w i^i S)) -> (u e. s -> (t e. u -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))))
61	60	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ S C_ X) -> (w e. J -> (u = (w i^i S) -> (u e. s -> (t e. u -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))))))
62	61	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . 22 |- ((J e. Top /\ S C_ X) -> (E.w e. J u = (w i^i S) -> (u e. s -> (t e. u -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))))
63	36, 62	sylbid 220	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ S C_ X) -> (u e. (subSp` <.S, J>.) -> (u e. s -> (t e. u -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))))
64	63	com23 36	. . . . . . . . . . . . . . . . . . . 20 |- ((J e. Top /\ S C_ X) -> (u e. s -> (u e. (subSp` <.S, J>.) -> (t e. u -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))))
65	64	com4l 43	. . . . . . . . . . . . . . . . . . 19 |- (u e. s -> (u e. (subSp` <.S, J>.) -> (t e. u -> ((J e. Top /\ S C_ X) -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))))
66	26, 65	sylcom 62	. . . . . . . . . . . . . . . . . 18 |- (s C_ (subSp` <.S, J>.) -> (u e. s -> (t e. u -> ((J e. Top /\ S C_ X) -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))))
67	66	com24 41	. . . . . . . . . . . . . . . . 17 |- (s C_ (subSp` <.S, J>.) -> ((J e. Top /\ S C_ X) -> (t e. u -> (u e. s -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))))
68	67	impcom 378	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ S C_ X) /\ s C_ (subSp` <.S, J>.)) -> (t e. u -> (u e. s -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))))
69	68	imp3a 388	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ S C_ X) /\ s C_ (subSp` <.S, J>.)) -> ((t e. u /\ u e. s) -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))
70	69	19.23adv 1584	. . . . . . . . . . . . . 14 |- (((J e. Top /\ S C_ X) /\ s C_ (subSp` <.S, J>.)) -> (E.u(t e. u /\ u e. s) -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))
71	70	adantr 425	. . . . . . . . . . . . 13 |- ((((J e. Top /\ S C_ X) /\ s C_ (subSp` <.S, J>.)) /\ S = U.s) -> (E.u(t e. u /\ u e. s) -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))
72	25, 71	sylbid 220	. . . . . . . . . . . 12 |- ((((J e. Top /\ S C_ X) /\ s C_ (subSp` <.S, J>.)) /\ S = U.s) -> (t e. S -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))
73	72	ex 402	. . . . . . . . . . 11 |- (((J e. Top /\ S C_ X) /\ s C_ (subSp` <.S, J>.)) -> (S = U.s -> (t e. S -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))))
74		visset 2295	. . . . . . . . . . . 12 |- s e. _V
75	74	elpw 3037	. . . . . . . . . . 11 |- (s e. ~P(subSp` <.S, J>.) <-> s C_ (subSp` <.S, J>.))
76	73, 75	sylan2b 501	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> (S = U.s -> (t e. S -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))))
77	76	imp 377	. . . . . . . . 9 |- ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> (t e. S -> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s})))
78		eluni 3180	. . . . . . . . 9 |- (t e. U.{y e. J | (y i^i S) e. s} <-> E.v(t e. v /\ v e. {y e. J | (y i^i S) e. s}))
79	77, 78	syl6ibr 230	. . . . . . . 8 |- ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> (t e. S -> t e. U.{y e. J | (y i^i S) e. s}))
80	79	ssrdv 2622	. . . . . . 7 |- ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> S C_ U.{y e. J | (y i^i S) e. s})
81		pm2.27 76	. . . . . . . . 9 |- (S C_ U.{y e. J | (y i^i S) e. s} -> ((S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d) -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d))
82		elin 2786	. . . . . . . . . . 11 |- (d e. (~P{y e. J | (y i^i S) e. s} i^i Fin) <-> (d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin))
83		elin 2786	. . . . . . . . . . . . . 14 |- ({x | E.z e. d x = (z i^i S)} e. (~Ps i^i Fin) <-> ({x | E.z e. d x = (z i^i S)} e. ~Ps /\ {x | E.z e. d x = (z i^i S)} e. Fin))
84		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (d C_ {y e. J | (y i^i S) e. s} -> (z e. d -> z e. {y e. J | (y i^i S) e. s}))
85		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y = z -> (y i^i S) = (z i^i S))
86	85	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y = z -> ((y i^i S) e. s <-> (z i^i S) e. s))
87	86	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. {y e. J | (y i^i S) e. s} <-> (z e. J /\ (z i^i S) e. s))
88		eleq1a 1966	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z i^i S) e. s -> (t = (z i^i S) -> t e. s))
89	88	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z e. J /\ (z i^i S) e. s) -> (t = (z i^i S) -> t e. s))
90	87, 89	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. {y e. J | (y i^i S) e. s} -> (t = (z i^i S) -> t e. s))
91	84, 90	syl6 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- (d C_ {y e. J | (y i^i S) e. s} -> (z e. d -> (t = (z i^i S) -> t e. s)))
92	91	a1d 15	. . . . . . . . . . . . . . . . . . . . . 22 |- (d C_ {y e. J | (y i^i S) e. s} -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> (z e. d -> (t = (z i^i S) -> t e. s))))
93	92	a1d 15	. . . . . . . . . . . . . . . . . . . . 21 |- (d C_ {y e. J | (y i^i S) e. s} -> (S C_ U.d -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> (z e. d -> (t = (z i^i S) -> t e. s)))))
94	93	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((d C_ {y e. J | (y i^i S) e. s} /\ d e. Fin) -> (S C_ U.d -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> (z e. d -> (t = (z i^i S) -> t e. s)))))
95		visset 2295	. . . . . . . . . . . . . . . . . . . . 21 |- d e. _V
96	95	elpw 3037	. . . . . . . . . . . . . . . . . . . 20 |- (d e. ~P{y e. J | (y i^i S) e. s} <-> d C_ {y e. J | (y i^i S) e. s})
97	94, 96	sylanb 498	. . . . . . . . . . . . . . . . . . 19 |- ((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) -> (S C_ U.d -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> (z e. d -> (t = (z i^i S) -> t e. s)))))
98	97	3imp 1061	. . . . . . . . . . . . . . . . . 18 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> (z e. d -> (t = (z i^i S) -> t e. s)))
99	98	r19.23adv 2215	. . . . . . . . . . . . . . . . 17 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> (E.z e. d t = (z i^i S) -> t e. s))
100		visset 2295	. . . . . . . . . . . . . . . . . 18 |- t e. _V
101		eqeq1 1890	. . . . . . . . . . . . . . . . . . 19 |- (x = t -> (x = (z i^i S) <-> t = (z i^i S)))
102	101	rexbidv 2124	. . . . . . . . . . . . . . . . . 18 |- (x = t -> (E.z e. d x = (z i^i S) <-> E.z e. d t = (z i^i S)))
103	100, 102	elab 2403	. . . . . . . . . . . . . . . . 17 |- (t e. {x | E.z e. d x = (z i^i S)} <-> E.z e. d t = (z i^i S))
104	99, 103	syl5ib 223	. . . . . . . . . . . . . . . 16 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> (t e. {x | E.z e. d x = (z i^i S)} -> t e. s))
105	104	ssrdv 2622	. . . . . . . . . . . . . . 15 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> {x | E.z e. d x = (z i^i S)} C_ s)
106	95	abrexex 4836	. . . . . . . . . . . . . . . 16 |- {x | E.z e. d x = (z i^i S)} e. _V
107	106	elpw 3037	. . . . . . . . . . . . . . 15 |- ({x | E.z e. d x = (z i^i S)} e. ~Ps <-> {x | E.z e. d x = (z i^i S)} C_ s)
108	105, 107	sylibr 217	. . . . . . . . . . . . . 14 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> {x | E.z e. d x = (z i^i S)} e. ~Ps)
109		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. _V
110	109	inex1 3452	. . . . . . . . . . . . . . . . . . . . 21 |- (z i^i S) e. _V
111		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- {<.z, x>. | (z e. d /\ x = (z i^i S))} = {<.z, x>. | (z e. d /\ x = (z i^i S))}
112	110, 111	fnopab2 4549	. . . . . . . . . . . . . . . . . . . 20 |- {<.z, x>. | (z e. d /\ x = (z i^i S))} Fn d
113		dffn4 4623	. . . . . . . . . . . . . . . . . . . 20 |- ({<.z, x>. | (z e. d /\ x = (z i^i S))} Fn d <-> {<.z, x>. | (z e. d /\ x = (z i^i S))}:d-onto->ran {<.z, x>. | (z e. d /\ x = (z i^i S))})
114	112, 113	mpbi 206	. . . . . . . . . . . . . . . . . . 19 |- {<.z, x>. | (z e. d /\ x = (z i^i S))}:d-onto->ran {<.z, x>. | (z e. d /\ x = (z i^i S))}
115		fodomfi 5656	. . . . . . . . . . . . . . . . . . 19 |- ((d e. Fin /\ {<.z, x>. | (z e. d /\ x = (z i^i S))}:d-onto->ran {<.z, x>. | (z e. d /\ x = (z i^i S))}) -> ran {<.z, x>. | (z e. d /\ x = (z i^i S))} ~<_ d)
116	114, 115	mpan2 760	. . . . . . . . . . . . . . . . . 18 |- (d e. Fin -> ran {<.z, x>. | (z e. d /\ x = (z i^i S))} ~<_ d)
117		domfi 5631	. . . . . . . . . . . . . . . . . 18 |- ((d e. Fin /\ ran {<.z, x>. | (z e. d /\ x = (z i^i S))} ~<_ d) -> ran {<.z, x>. | (z e. d /\ x = (z i^i S))} e. Fin)
118	116, 117	mpdan 768	. . . . . . . . . . . . . . . . 17 |- (d e. Fin -> ran {<.z, x>. | (z e. d /\ x = (z i^i S))} e. Fin)
119		rnopab2 4202	. . . . . . . . . . . . . . . . 17 |- ran {<.z, x>. | (z e. d /\ x = (z i^i S))} = {x | E.z e. d x = (z i^i S)}
120	118, 119	syl5eqelr 1976	. . . . . . . . . . . . . . . 16 |- (d e. Fin -> {x | E.z e. d x = (z i^i S)} e. Fin)
121	120	ad2antlr 441	. . . . . . . . . . . . . . 15 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d) -> {x | E.z e. d x = (z i^i S)} e. Fin)
122	121	3adant3 896	. . . . . . . . . . . . . 14 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> {x | E.z e. d x = (z i^i S)} e. Fin)
123	83, 108, 122	sylanbrc 527	. . . . . . . . . . . . 13 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> {x | E.z e. d x = (z i^i S)} e. (~Ps i^i Fin))
124	20	ad2antrl 442	. . . . . . . . . . . . . . 15 |- ((S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> U.(subSp` <.S, J>.) = S)
125	124	3adant1 894	. . . . . . . . . . . . . 14 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> U.(subSp` <.S, J>.) = S)
126		dfss 2606	. . . . . . . . . . . . . . . . 17 |- (S C_ U.d <-> S = (S i^i U.d))
127	126	biimpi 168	. . . . . . . . . . . . . . . 16 |- (S C_ U.d -> S = (S i^i U.d))
128		uniiun 3306	. . . . . . . . . . . . . . . . . 18 |- U.d = U_z e. d z
129	128	ineq2i 2793	. . . . . . . . . . . . . . . . 17 |- (S i^i U.d) = (S i^i U_z e. d z)
130		iunin2 3320	. . . . . . . . . . . . . . . . 17 |- U_z e. d (S i^i z) = (S i^i U_z e. d z)
131		incom 2787	. . . . . . . . . . . . . . . . . . 19 |- (S i^i z) = (z i^i S)
132	131	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (z e. d -> (S i^i z) = (z i^i S))
133	132	iuneq2i 3276	. . . . . . . . . . . . . . . . 17 |- U_z e. d (S i^i z) = U_z e. d (z i^i S)
134	129, 130, 133	3eqtr2i 1915	. . . . . . . . . . . . . . . 16 |- (S i^i U.d) = U_z e. d (z i^i S)
135	127, 134	syl6eq 1944	. . . . . . . . . . . . . . 15 |- (S C_ U.d -> S = U_z e. d (z i^i S))
136	135	3ad2ant2 898	. . . . . . . . . . . . . 14 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> S = U_z e. d (z i^i S))
137	110	dfiun2 3285	. . . . . . . . . . . . . . 15 |- U_z e. d (z i^i S) = U.{x | E.z e. d x = (z i^i S)}
138	137	a1i 8	. . . . . . . . . . . . . 14 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> U_z e. d (z i^i S) = U.{x | E.z e. d x = (z i^i S)})
139	125, 136, 138	3eqtrd 1929	. . . . . . . . . . . . 13 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> U.(subSp` <.S, J>.) = U.{x | E.z e. d x = (z i^i S)})
140		unieq 3185	. . . . . . . . . . . . . . 15 |- (t = {x | E.z e. d x = (z i^i S)} -> U.t = U.{x | E.z e. d x = (z i^i S)})
141	140	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (t = {x | E.z e. d x = (z i^i S)} -> (U.(subSp` <.S, J>.) = U.t <-> U.(subSp` <.S, J>.) = U.{x | E.z e. d x = (z i^i S)}))
142	141	rcla4ev 2381	. . . . . . . . . . . . 13 |- (({x | E.z e. d x = (z i^i S)} e. (~Ps i^i Fin) /\ U.(subSp` <.S, J>.) = U.{x | E.z e. d x = (z i^i S)}) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)
143	123, 139, 142	syl11anc 524	. . . . . . . . . . . 12 |- (((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) /\ S C_ U.d /\ (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s)) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)
144	143	3exp 1066	. . . . . . . . . . 11 |- ((d e. ~P{y e. J | (y i^i S) e. s} /\ d e. Fin) -> (S C_ U.d -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
145	82, 144	sylbi 216	. . . . . . . . . 10 |- (d e. (~P{y e. J | (y i^i S) e. s} i^i Fin) -> (S C_ U.d -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
146	145	r19.23aiv 2211	. . . . . . . . 9 |- (E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t))
147	81, 146	syl6 25	. . . . . . . 8 |- (S C_ U.{y e. J | (y i^i S) e. s} -> ((S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d) -> ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
148	147	com3r 39	. . . . . . 7 |- ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> (S C_ U.{y e. J | (y i^i S) e. s} -> ((S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
149	80, 148	mpd 29	. . . . . 6 |- ((((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) /\ S = U.s) -> ((S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t))
150	149	ex 402	. . . . 5 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> (S = U.s -> ((S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
151	21, 150	sylbid 220	. . . 4 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> (U.(subSp` <.S, J>.) = U.s -> ((S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d) -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
152	151	com23 36	. . 3 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> ((S C_ U.{y e. J | (y i^i S) e. s} -> E.d e. (~P{y e. J | (y i^i S) e. s} i^i Fin)S C_ U.d) -> (U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
153	15, 152	syld 30	. 2 |- (((J e. Top /\ S C_ X) /\ s e. ~P(subSp` <.S, J>.)) -> (A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d) -> (U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
154	153	r19.21adva 2182	1 |- ((J e. Top /\ S C_ X) -> (A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d) -> A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   i^i cin 2592   C_ wss 2593  ~Pcpw 3032  <.cop 3046  U.cuni 3177  U_ciun 3255   class class class wbr 3338  {copab 3395  ran crn 3987   Fn wfn 3993  -onto->wfo 3996  ` cfv 3998   ~<_ cdom 5424  Fincfn 5426  Topctop 8857  subSpcsubsp 10242

This theorem is referenced by:  compsub 15431

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  ax-reg 5695

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-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-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-1o 5177  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-top 8861  df-topsp 8862  df-subsp 10243

Copyright terms: Public domain