Theorem compsublem 11480

Description: Lemma for compsub 11481.

Hypothesis

Ref	Expression
compsub.1	⊢ X = ∪J

Assertion

Ref	Expression
compsublem	⊢ ((J ∈ Top ⋀ S ⊆ X) → (∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d) → ∀s ∈ ℘ (subSp ‘<.S, J>.)(∪(subSp ‘<.S, J>.) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪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 2576	. . . . . . . 8 ⊢ (c = {y ∈ J∣(y ∩ S) ∈ s} → ∪c = ∪{y ∈ J∣(y ∩ S) ∈ s})
2	1	sseq2d 2141	. . . . . . 7 ⊢ (c = {y ∈ J∣(y ∩ S) ∈ s} → (S ⊆ ∪c ↔ S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s}))
3		pweq 2460	. . . . . . . . 9 ⊢ (c = {y ∈ J∣(y ∩ S) ∈ s} → ℘c = ℘{y ∈ J∣(y ∩ S) ∈ s})
4	3	ineq1d 2268	. . . . . . . 8 ⊢ (c = {y ∈ J∣(y ∩ S) ∈ s} → (℘c ∩ Fin) = (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin))
5	4	rexeq1d 1836	. . . . . . 7 ⊢ (c = {y ∈ J∣(y ∩ S) ∈ s} → (∃d ∈ (℘c ∩ Fin)S ⊆ ∪d ↔ ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d))
6	2, 5	imbi12d 629	. . . . . 6 ⊢ (c = {y ∈ J∣(y ∩ S) ∈ s} → ((S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d) ↔ (S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d)))
7	6	rcla4va 1921	. . . . 5 ⊢ (({y ∈ J∣(y ∩ S) ∈ s} ∈ ℘J ⋀ ∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)) → (S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d))
8		rabexg 2798	. . . . . . 7 ⊢ (J ∈ Top → {y ∈ J∣(y ∩ S) ∈ s} ∈ V)
9	8	ad2antrr 404	. . . . . 6 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → {y ∈ J∣(y ∩ S) ∈ s} ∈ V)
10		ssrab2 2183	. . . . . . 7 ⊢ {y ∈ J∣(y ∩ S) ∈ s} ⊆ J
11		elpwg 2462	. . . . . . 7 ⊢ ({y ∈ J∣(y ∩ S) ∈ s} ∈ V → ({y ∈ J∣(y ∩ S) ∈ s} ∈ ℘J ↔ {y ∈ J∣(y ∩ S) ∈ s} ⊆ J))
12	10, 11	mpbiri 192	. . . . . 6 ⊢ ({y ∈ J∣(y ∩ S) ∈ s} ∈ V → {y ∈ J∣(y ∩ S) ∈ s} ∈ ℘J)
13	9, 12	syl 10	. . . . 5 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → {y ∈ J∣(y ∩ S) ∈ s} ∈ ℘J)
14	7, 13	sylan 450	. . . 4 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ ∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)) → (S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d))
15	14	ex 371	. . 3 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → (∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d) → (S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d)))
16		stoig2 11056	. . . . . . . 8 ⊢ ((J ∈ Top ⋀ S ⊆ ∪J) → ∪(subSp ‘<.S, J>.) = S)
17		compsub.1	. . . . . . . . 9 ⊢ X = ∪J
18	17	sseq2i 2138	. . . . . . . 8 ⊢ (S ⊆ X ↔ S ⊆ ∪J)
19	16, 18	sylan2b 454	. . . . . . 7 ⊢ ((J ∈ Top ⋀ S ⊆ X) → ∪(subSp ‘<.S, J>.) = S)
20	19	adantr 389	. . . . . 6 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → ∪(subSp ‘<.S, J>.) = S)
21	20	eqeq1d 1526	. . . . 5 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → (∪(subSp ‘<.S, J>.) = ∪s ↔ S = ∪s))
22		eleq2 1578	. . . . . . . . . . . . . . 15 ⊢ (S = ∪s → (t ∈ S ↔ t ∈ ∪s))
23		eluni 2572	. . . . . . . . . . . . . . 15 ⊢ (t ∈ ∪s ↔ ∃u(t ∈ u ⋀ u ∈ s))
24	22, 23	syl6bb 539	. . . . . . . . . . . . . 14 ⊢ (S = ∪s → (t ∈ S ↔ ∃u(t ∈ u ⋀ u ∈ s)))
25	24	adantl 388	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ⊆ (subSp ‘<.S, J>.)) ⋀ S = ∪s) → (t ∈ S ↔ ∃u(t ∈ u ⋀ u ∈ s)))
26		ssel 2115	. . . . . . . . . . . . . . . . . . 19 ⊢ (s ⊆ (subSp ‘<.S, J>.) → (u ∈ s → u ∈ (subSp ‘<.S, J>.)))
27		issubspt 11050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((J ∈ Top ⋀ u ∈ V ⋀ S ∈ V) → (u ∈ (subSp ‘<.S, J>.) ↔ ∃w ∈ J u = (w ∩ S)))
28		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((J ∈ Top ⋀ S ⊆ X) → J ∈ Top)
29		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ u ∈ V
30	29	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((J ∈ Top ⋀ S ⊆ X) → u ∈ V)
31		ssexg 2795	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((S ⊆ ∪J ⋀ ∪J ∈ V) → S ∈ V)
32	31	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∪J ∈ V ⋀ S ⊆ ∪J) → S ∈ V)
33		uniexg 3094	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (J ∈ Top → ∪J ∈ V)
34	32, 33	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((J ∈ Top ⋀ S ⊆ ∪J) → S ∈ V)
35	34, 18	sylan2b 454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((J ∈ Top ⋀ S ⊆ X) → S ∈ V)
36	27, 28, 30, 35	syl3anc 864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (u ∈ (subSp ‘<.S, J>.) ↔ ∃w ∈ J u = (w ∩ S)))
37		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ w ∈ V
38		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (v = w → (t ∈ v ↔ t ∈ w))
39		eleq1 1577	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (v = w → (v ∈ {y ∈ J∣(y ∩ S) ∈ s} ↔ w ∈ {y ∈ J∣(y ∩ S) ∈ s}))
40	38, 39	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v = w → ((t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}) ↔ (t ∈ w ⋀ w ∈ {y ∈ J∣(y ∩ S) ∈ s})))
41	37, 40	cla4ev 1915	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((t ∈ w ⋀ w ∈ {y ∈ J∣(y ∩ S) ∈ s}) → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))
42		ssel2 2116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((u ⊆ w ⋀ t ∈ u) → t ∈ w)
43		inss1 2282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w ∩ S) ⊆ w
44		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (u = (w ∩ S) → (u ⊆ w ↔ (w ∩ S) ⊆ w))
45	43, 44	mpbiri 192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (u = (w ∩ S) → u ⊆ w)
46	42, 45	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((u = (w ∩ S) ⋀ t ∈ u) → t ∈ w)
47	46	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ t ∈ u) → t ∈ w)
48	47	3adant2 804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ u ∈ s ⋀ t ∈ u) → t ∈ w)
49		3simp2 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) → w ∈ J)
50	49	3ad2ant1 806	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ u ∈ s ⋀ t ∈ u) → w ∈ J)
51		eleq1 1577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (u = (w ∩ S) → (u ∈ s ↔ (w ∩ S) ∈ s))
52	51	biimpa 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((u = (w ∩ S) ⋀ u ∈ s) → (w ∩ S) ∈ s)
53	52	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ u ∈ s) → (w ∩ S) ∈ s)
54	53	3adant3 805	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ u ∈ s ⋀ t ∈ u) → (w ∩ S) ∈ s)
55	50, 54	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ u ∈ s ⋀ t ∈ u) → (w ∈ J ⋀ (w ∩ S) ∈ s))
56		ineq1 2262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y = w → (y ∩ S) = (w ∩ S))
57	56	eleq1d 1583	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (y = w → ((y ∩ S) ∈ s ↔ (w ∩ S) ∈ s))
58	57	elrab 1951	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (w ∈ {y ∈ J∣(y ∩ S) ∈ s} ↔ (w ∈ J ⋀ (w ∩ S) ∈ s))
59	55, 58	sylibr 198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ u ∈ s ⋀ t ∈ u) → w ∈ {y ∈ J∣(y ∩ S) ∈ s})
60	41, 48, 59	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) ⋀ u ∈ s ⋀ t ∈ u) → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))
61	60	3exp 838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ w ∈ J ⋀ u = (w ∩ S)) → (u ∈ s → (t ∈ u → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))))
62	61	3exp 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (w ∈ J → (u = (w ∩ S) → (u ∈ s → (t ∈ u → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))))))
63	62	r19.23adv 1792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (∃w ∈ J u = (w ∩ S) → (u ∈ s → (t ∈ u → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))))
64	36, 63	sylbid 201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (u ∈ (subSp ‘<.S, J>.) → (u ∈ s → (t ∈ u → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))))
65	64	com23 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (u ∈ s → (u ∈ (subSp ‘<.S, J>.) → (t ∈ u → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))))
66	65	com4l 39	. . . . . . . . . . . . . . . . . . 19 ⊢ (u ∈ s → (u ∈ (subSp ‘<.S, J>.) → (t ∈ u → ((J ∈ Top ⋀ S ⊆ X) → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))))
67	26, 66	sylcom 51	. . . . . . . . . . . . . . . . . 18 ⊢ (s ⊆ (subSp ‘<.S, J>.) → (u ∈ s → (t ∈ u → ((J ∈ Top ⋀ S ⊆ X) → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))))
68	67	com24 37	. . . . . . . . . . . . . . . . 17 ⊢ (s ⊆ (subSp ‘<.S, J>.) → ((J ∈ Top ⋀ S ⊆ X) → (t ∈ u → (u ∈ s → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))))
69	68	impcom 349	. . . . . . . . . . . . . . . 16 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ⊆ (subSp ‘<.S, J>.)) → (t ∈ u → (u ∈ s → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))))
70	69	imp3a 359	. . . . . . . . . . . . . . 15 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ⊆ (subSp ‘<.S, J>.)) → ((t ∈ u ⋀ u ∈ s) → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))
71	70	19.23adv 1251	. . . . . . . . . . . . . 14 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ⊆ (subSp ‘<.S, J>.)) → (∃u(t ∈ u ⋀ u ∈ s) → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))
72	71	adantr 389	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ⊆ (subSp ‘<.S, J>.)) ⋀ S = ∪s) → (∃u(t ∈ u ⋀ u ∈ s) → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))
73	25, 72	sylbid 201	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ⊆ (subSp ‘<.S, J>.)) ⋀ S = ∪s) → (t ∈ S → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))
74	73	ex 371	. . . . . . . . . . 11 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ⊆ (subSp ‘<.S, J>.)) → (S = ∪s → (t ∈ S → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))))
75		visset 1859	. . . . . . . . . . . 12 ⊢ s ∈ V
76	75	elpw 2461	. . . . . . . . . . 11 ⊢ (s ∈ ℘(subSp ‘<.S, J>.) ↔ s ⊆ (subSp ‘<.S, J>.))
77	74, 76	sylan2b 454	. . . . . . . . . 10 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → (S = ∪s → (t ∈ S → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))))
78	77	imp 348	. . . . . . . . 9 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → (t ∈ S → ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s})))
79		eluni 2572	. . . . . . . . 9 ⊢ (t ∈ ∪{y ∈ J∣(y ∩ S) ∈ s} ↔ ∃v(t ∈ v ⋀ v ∈ {y ∈ J∣(y ∩ S) ∈ s}))
80	78, 79	syl6ibr 211	. . . . . . . 8 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → (t ∈ S → t ∈ ∪{y ∈ J∣(y ∩ S) ∈ s}))
81	80	ssrdv 2122	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s})
82		pm2.27 62	. . . . . . . . 9 ⊢ (S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ((S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d) → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d))
83		elin 2259	. . . . . . . . . . 11 ⊢ (d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin) ↔ (d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin))
84		unieq 2576	. . . . . . . . . . . . . . 15 ⊢ (t = {x∣∃z ∈ d x = (z ∩ S)} → ∪t = ∪{x∣∃z ∈ d x = (z ∩ S)})
85	84	eqeq2d 1529	. . . . . . . . . . . . . 14 ⊢ (t = {x∣∃z ∈ d x = (z ∩ S)} → (∪(subSp ‘<.S, J>.) = ∪t ↔ ∪(subSp ‘<.S, J>.) = ∪{x∣∃z ∈ d x = (z ∩ S)}))
86	85	rcla4ev 1923	. . . . . . . . . . . . 13 ⊢ (({x∣∃z ∈ d x = (z ∩ S)} ∈ (℘s ∩ Fin) ⋀ ∪(subSp ‘<.S, J>.) = ∪{x∣∃z ∈ d x = (z ∩ S)}) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)
87		ssel 2115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (d ⊆ {y ∈ J∣(y ∩ S) ∈ s} → (z ∈ d → z ∈ {y ∈ J∣(y ∩ S) ∈ s}))
88		ineq1 2262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (y = z → (y ∩ S) = (z ∩ S))
89	88	eleq1d 1583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (y = z → ((y ∩ S) ∈ s ↔ (z ∩ S) ∈ s))
90	89	elrab 1951	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (z ∈ {y ∈ J∣(y ∩ S) ∈ s} ↔ (z ∈ J ⋀ (z ∩ S) ∈ s))
91		eleq1a 1586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((z ∩ S) ∈ s → (t = (z ∩ S) → t ∈ s))
92	91	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((z ∈ J ⋀ (z ∩ S) ∈ s) → (t = (z ∩ S) → t ∈ s))
93	90, 92	sylbi 197	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (z ∈ {y ∈ J∣(y ∩ S) ∈ s} → (t = (z ∩ S) → t ∈ s))
94	87, 93	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (d ⊆ {y ∈ J∣(y ∩ S) ∈ s} → (z ∈ d → (t = (z ∩ S) → t ∈ s)))
95	94	a1d 12	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (d ⊆ {y ∈ J∣(y ∩ S) ∈ s} → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → (z ∈ d → (t = (z ∩ S) → t ∈ s))))
96	95	a1d 12	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (d ⊆ {y ∈ J∣(y ∩ S) ∈ s} → (S ⊆ ∪d → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → (z ∈ d → (t = (z ∩ S) → t ∈ s)))))
97	96	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((d ⊆ {y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) → (S ⊆ ∪d → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → (z ∈ d → (t = (z ∩ S) → t ∈ s)))))
98		visset 1859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ d ∈ V
99	98	elpw 2461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ↔ d ⊆ {y ∈ J∣(y ∩ S) ∈ s})
100	97, 99	sylanb 451	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) → (S ⊆ ∪d → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → (z ∈ d → (t = (z ∩ S) → t ∈ s)))))
101	100	3imp 833	. . . . . . . . . . . . . . . . . . 19 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → (z ∈ d → (t = (z ∩ S) → t ∈ s)))
102	101	r19.23adv 1792	. . . . . . . . . . . . . . . . . 18 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → (∃z ∈ d t = (z ∩ S) → t ∈ s))
103		visset 1859	. . . . . . . . . . . . . . . . . . 19 ⊢ t ∈ V
104		eqeq1 1524	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = t → (x = (z ∩ S) ↔ t = (z ∩ S)))
105	104	rexbidv 1710	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = t → (∃z ∈ d x = (z ∩ S) ↔ ∃z ∈ d t = (z ∩ S)))
106	103, 105	elab 1943	. . . . . . . . . . . . . . . . . 18 ⊢ (t ∈ {x∣∃z ∈ d x = (z ∩ S)} ↔ ∃z ∈ d t = (z ∩ S))
107	102, 106	syl5ib 204	. . . . . . . . . . . . . . . . 17 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → (t ∈ {x∣∃z ∈ d x = (z ∩ S)} → t ∈ s))
108	107	ssrdv 2122	. . . . . . . . . . . . . . . 16 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → {x∣∃z ∈ d x = (z ∩ S)} ⊆ s)
109	98	abrexex 3974	. . . . . . . . . . . . . . . . 17 ⊢ {x∣∃z ∈ d x = (z ∩ S)} ∈ V
110	109	elpw 2461	. . . . . . . . . . . . . . . 16 ⊢ ({x∣∃z ∈ d x = (z ∩ S)} ∈ ℘s ↔ {x∣∃z ∈ d x = (z ∩ S)} ⊆ s)
111	108, 110	sylibr 198	. . . . . . . . . . . . . . 15 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → {x∣∃z ∈ d x = (z ∩ S)} ∈ ℘s)
112		visset 1859	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ z ∈ V
113	112	inex1 2790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z ∩ S) ∈ V
114		eqid 1518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} = {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))}
115	113, 114	fnopab2 3725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} Fn d
116		dffn4 3785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} Fn d ↔ {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))}:d–onto→ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))})
117	115, 116	mpbi 187	. . . . . . . . . . . . . . . . . . . 20 ⊢ {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))}:d–onto→ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))}
118		fodomfi 4709	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((d ∈ Fin ⋀ {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))}:d–onto→ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))}) → ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} ≼ d)
119	117, 118	mpan2 700	. . . . . . . . . . . . . . . . . . 19 ⊢ (d ∈ Fin → ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} ≼ d)
120		domfi 4684	. . . . . . . . . . . . . . . . . . 19 ⊢ ((d ∈ Fin ⋀ ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} ≼ d) → ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} ∈ Fin)
121	119, 120	mpdan 708	. . . . . . . . . . . . . . . . . 18 ⊢ (d ∈ Fin → ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} ∈ Fin)
122		rnopab2 3441	. . . . . . . . . . . . . . . . . 18 ⊢ ran {<.z, x>.∣(z ∈ d ⋀ x = (z ∩ S))} = {x∣∃z ∈ d x = (z ∩ S)}
123	121, 122	syl5eqelr 1596	. . . . . . . . . . . . . . . . 17 ⊢ (d ∈ Fin → {x∣∃z ∈ d x = (z ∩ S)} ∈ Fin)
124	123	ad2antlr 405	. . . . . . . . . . . . . . . 16 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d) → {x∣∃z ∈ d x = (z ∩ S)} ∈ Fin)
125	124	3adant3 805	. . . . . . . . . . . . . . 15 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → {x∣∃z ∈ d x = (z ∩ S)} ∈ Fin)
126	111, 125	jca 286	. . . . . . . . . . . . . 14 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → ({x∣∃z ∈ d x = (z ∩ S)} ∈ ℘s ⋀ {x∣∃z ∈ d x = (z ∩ S)} ∈ Fin))
127		elin 2259	. . . . . . . . . . . . . 14 ⊢ ({x∣∃z ∈ d x = (z ∩ S)} ∈ (℘s ∩ Fin) ↔ ({x∣∃z ∈ d x = (z ∩ S)} ∈ ℘s ⋀ {x∣∃z ∈ d x = (z ∩ S)} ∈ Fin))
128	126, 127	sylibr 198	. . . . . . . . . . . . 13 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → {x∣∃z ∈ d x = (z ∩ S)} ∈ (℘s ∩ Fin))
129	20	ad2antrl 406	. . . . . . . . . . . . . . 15 ⊢ ((S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → ∪(subSp ‘<.S, J>.) = S)
130	129	3adant1 803	. . . . . . . . . . . . . 14 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → ∪(subSp ‘<.S, J>.) = S)
131		dfss 2106	. . . . . . . . . . . . . . . . 17 ⊢ (S ⊆ ∪d ↔ S = (S ∩ ∪d))
132	131	biimpi 149	. . . . . . . . . . . . . . . 16 ⊢ (S ⊆ ∪d → S = (S ∩ ∪d))
133		uniiun 2669	. . . . . . . . . . . . . . . . . 18 ⊢ ∪d = ∪z ∈ d z
134	133	ineq2i 2266	. . . . . . . . . . . . . . . . 17 ⊢ (S ∩ ∪d) = (S ∩ ∪z ∈ d z)
135		iunin2 2677	. . . . . . . . . . . . . . . . 17 ⊢ ∪z ∈ d (S ∩ z) = (S ∩ ∪z ∈ d z)
136		incom 2260	. . . . . . . . . . . . . . . . . . 19 ⊢ (S ∩ z) = (z ∩ S)
137	136	a1i 8	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ d → (S ∩ z) = (z ∩ S))
138	137	iuneq2i 2648	. . . . . . . . . . . . . . . . 17 ⊢ ∪z ∈ d (S ∩ z) = ∪z ∈ d (z ∩ S)
139	134, 135, 138	3eqtr2i 1544	. . . . . . . . . . . . . . . 16 ⊢ (S ∩ ∪d) = ∪z ∈ d (z ∩ S)
140	132, 139	syl6eq 1566	. . . . . . . . . . . . . . 15 ⊢ (S ⊆ ∪d → S = ∪z ∈ d (z ∩ S))
141	140	3ad2ant2 807	. . . . . . . . . . . . . 14 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → S = ∪z ∈ d (z ∩ S))
142	113	dfiun2 2655	. . . . . . . . . . . . . . 15 ⊢ ∪z ∈ d (z ∩ S) = ∪{x∣∃z ∈ d x = (z ∩ S)}
143	142	a1i 8	. . . . . . . . . . . . . 14 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → ∪z ∈ d (z ∩ S) = ∪{x∣∃z ∈ d x = (z ∩ S)})
144	130, 141, 143	3eqtrd 1554	. . . . . . . . . . . . 13 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → ∪(subSp ‘<.S, J>.) = ∪{x∣∃z ∈ d x = (z ∩ S)})
145	86, 128, 144	sylanc 473	. . . . . . . . . . . 12 ⊢ (((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) ⋀ S ⊆ ∪d ⋀ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s)) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)
146	145	3exp 838	. . . . . . . . . . 11 ⊢ ((d ∈ ℘{y ∈ J∣(y ∩ S) ∈ s} ⋀ d ∈ Fin) → (S ⊆ ∪d → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
147	83, 146	sylbi 197	. . . . . . . . . 10 ⊢ (d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin) → (S ⊆ ∪d → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
148	147	r19.23aiv 1789	. . . . . . . . 9 ⊢ (∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t))
149	82, 148	syl6 22	. . . . . . . 8 ⊢ (S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ((S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d) → ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
150	149	com3r 35	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → (S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ((S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
151	81, 150	mpd 26	. . . . . 6 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) ⋀ S = ∪s) → ((S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t))
152	151	ex 371	. . . . 5 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → (S = ∪s → ((S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
153	21, 152	sylbid 201	. . . 4 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → (∪(subSp ‘<.S, J>.) = ∪s → ((S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d) → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
154	153	com23 32	. . 3 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → ((S ⊆ ∪{y ∈ J∣(y ∩ S) ∈ s} → ∃d ∈ (℘{y ∈ J∣(y ∩ S) ∈ s} ∩ Fin)S ⊆ ∪d) → (∪(subSp ‘<.S, J>.) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
155	15, 154	syld 27	. 2 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ s ∈ ℘(subSp ‘<.S, J>.)) → (∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d) → (∪(subSp ‘<.S, J>.) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))
156	155	r19.21adva 1765	1 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d) → ∀s ∈ ℘ (subSp ‘<.S, J>.)(∪(subSp ‘<.S, J>.) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘<.S, J>.) = ∪t)))

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   ⋀ w3a 781   = wceq 992   ∈ wcel 994  ∃wex 1016  {cab 1505  ∀wral 1691  ∃wrex 1692  {crab 1694  Vcvv 1857   ∩ cin 2098   ⊆ wss 2099  ℘cpw 2458  <.cop 2469  ∪cuni 2569  ∪ciun 2633   class class class wbr 2692  {copab 2740  ran crn 3252   Fn wfn 3258  –onto→wfo 3261   ‘cfv 3263   ≼ cdom 4506  Fincfn 4508  Topctop 7800  subSpcsubsp 11045

This theorem is referenced by:  compsub 11481

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-reg 4736

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1o 4269  df-er 4401  df-en 4509  df-dom 4510  df-fin 4512  df-top 7804  df-topsp 7805  df-subsp 11046

Copyright terms: Public domain