Theorem 2ndcctbss 15478

Description: If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard.

Hypotheses

Ref	Expression
2ndcctbss.1	|- X = U.B
2ndcctbss.2	|- J = (topGen` B)

Assertion

Ref	Expression
2ndcctbss	|- ((B e. Bases /\ J e. 2ndc) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b)))

Distinct variable groups:   B,b   J,b   X,b

Proof of Theorem 2ndcctbss

Step	Hyp	Ref	Expression
1		2ndccb 15475	. . 3 |- (J e. 2ndc -> E.c e. Bases (c ~<_ om /\ (topGen` c) = J))
2	1	adantl 424	. 2 |- ((B e. Bases /\ J e. 2ndc) -> E.c e. Bases (c ~<_ om /\ (topGen` c) = J))
3		sseq1 2637	. . . . . . . . . . . . . . . . . . 19 |- ((1st` x) = u -> ((1st` x) C_ w <-> u C_ w))
4	3	anbi1d 679	. . . . . . . . . . . . . . . . . 18 |- ((1st` x) = u -> (((1st` x) C_ w /\ w C_ (2nd` x)) <-> (u C_ w /\ w C_ (2nd` x))))
5	4	rexbidv 2124	. . . . . . . . . . . . . . . . 17 |- ((1st` x) = u -> (E.w e. B ((1st` x) C_ w /\ w C_ (2nd` x)) <-> E.w e. B (u C_ w /\ w C_ (2nd` x))))
6		sseq2 2639	. . . . . . . . . . . . . . . . . . 19 |- ((2nd` x) = v -> (w C_ (2nd` x) <-> w C_ v))
7	6	anbi2d 678	. . . . . . . . . . . . . . . . . 18 |- ((2nd` x) = v -> ((u C_ w /\ w C_ (2nd` x)) <-> (u C_ w /\ w C_ v)))
8	7	rexbidv 2124	. . . . . . . . . . . . . . . . 17 |- ((2nd` x) = v -> (E.w e. B (u C_ w /\ w C_ (2nd` x)) <-> E.w e. B (u C_ w /\ w C_ v)))
9	5, 8	sylan9bb 599	. . . . . . . . . . . . . . . 16 |- (((1st` x) = u /\ (2nd` x) = v) -> (E.w e. B ((1st` x) C_ w /\ w C_ (2nd` x)) <-> E.w e. B (u C_ w /\ w C_ v)))
10		sseq2 2639	. . . . . . . . . . . . . . . . . . 19 |- (w = y -> ((1st` x) C_ w <-> (1st` x) C_ y))
11		sseq1 2637	. . . . . . . . . . . . . . . . . . 19 |- (w = y -> (w C_ (2nd` x) <-> y C_ (2nd` x)))
12	10, 11	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- (w = y -> (((1st` x) C_ w /\ w C_ (2nd` x)) <-> ((1st` x) C_ y /\ y C_ (2nd` x))))
13	12	cbvrexv 2281	. . . . . . . . . . . . . . . . 17 |- (E.w e. B ((1st` x) C_ w /\ w C_ (2nd` x)) <-> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x)))
14	13	biimpi 168	. . . . . . . . . . . . . . . 16 |- (E.w e. B ((1st` x) C_ w /\ w C_ (2nd` x)) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x)))
15	9, 14	syl6bir 232	. . . . . . . . . . . . . . 15 |- (((1st` x) = u /\ (2nd` x) = v) -> (E.w e. B (u C_ w /\ w C_ v) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x))))
16	15	com12 14	. . . . . . . . . . . . . 14 |- (E.w e. B (u C_ w /\ w C_ v) -> (((1st` x) = u /\ (2nd` x) = v) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x))))
17	16	3ad2ant3 899	. . . . . . . . . . . . 13 |- ((u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v)) -> (((1st` x) = u /\ (2nd` x) = v) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x))))
18	17	com12 14	. . . . . . . . . . . 12 |- (((1st` x) = u /\ (2nd` x) = v) -> ((u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v)) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x))))
19	18	a1i 8	. . . . . . . . . . 11 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> (((1st` x) = u /\ (2nd` x) = v) -> ((u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v)) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x)))))
20		fveq2 4681	. . . . . . . . . . . . 13 |- (x = <.u, v>. -> (1st` x) = (1st` <.u, v>.))
21		visset 2295	. . . . . . . . . . . . . 14 |- u e. _V
22	21	op1st 5026	. . . . . . . . . . . . 13 |- (1st` <.u, v>.) = u
23	20, 22	syl6eq 1944	. . . . . . . . . . . 12 |- (x = <.u, v>. -> (1st` x) = u)
24		fveq2 4681	. . . . . . . . . . . . 13 |- (x = <.u, v>. -> (2nd` x) = (2nd` <.u, v>.))
25		visset 2295	. . . . . . . . . . . . . 14 |- v e. _V
26	21, 25	op2nd 5027	. . . . . . . . . . . . 13 |- (2nd` <.u, v>.) = v
27	24, 26	syl6eq 1944	. . . . . . . . . . . 12 |- (x = <.u, v>. -> (2nd` x) = v)
28	23, 27	jca 310	. . . . . . . . . . 11 |- (x = <.u, v>. -> ((1st` x) = u /\ (2nd` x) = v))
29	19, 28	syl5 20	. . . . . . . . . 10 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> (x = <.u, v>. -> ((u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v)) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x)))))
30	29	imp3a 388	. . . . . . . . 9 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> ((x = <.u, v>. /\ (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x))))
31	30	19.23advv 1676	. . . . . . . 8 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> (E.uE.v(x = <.u, v>. /\ (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))) -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x))))
32		elopab 3559	. . . . . . . 8 |- (x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} <-> E.uE.v(x = <.u, v>. /\ (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))))
33	31, 32	syl5ib 223	. . . . . . 7 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> (x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} -> E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x))))
34	33	r19.21aiv 2175	. . . . . 6 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x)))
35		visset 2295	. . . . . . . . 9 |- c e. _V
36	35, 35	xpex 4096	. . . . . . . 8 |- (c X. c) e. _V
37		relopab 4104	. . . . . . . . 9 |- Rel {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}
38		visset 2295	. . . . . . . . . . 11 |- r e. _V
39		visset 2295	. . . . . . . . . . 11 |- s e. _V
40		eleq1 1957	. . . . . . . . . . . 12 |- (u = r -> (u e. c <-> r e. c))
41		sseq1 2637	. . . . . . . . . . . . . 14 |- (u = r -> (u C_ w <-> r C_ w))
42	41	anbi1d 679	. . . . . . . . . . . . 13 |- (u = r -> ((u C_ w /\ w C_ v) <-> (r C_ w /\ w C_ v)))
43	42	rexbidv 2124	. . . . . . . . . . . 12 |- (u = r -> (E.w e. B (u C_ w /\ w C_ v) <-> E.w e. B (r C_ w /\ w C_ v)))
44	40, 43	3anbi13d 1170	. . . . . . . . . . 11 |- (u = r -> ((u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v)) <-> (r e. c /\ v e. c /\ E.w e. B (r C_ w /\ w C_ v))))
45		eleq1 1957	. . . . . . . . . . . 12 |- (v = s -> (v e. c <-> s e. c))
46		sseq2 2639	. . . . . . . . . . . . . 14 |- (v = s -> (w C_ v <-> w C_ s))
47	46	anbi2d 678	. . . . . . . . . . . . 13 |- (v = s -> ((r C_ w /\ w C_ v) <-> (r C_ w /\ w C_ s)))
48	47	rexbidv 2124	. . . . . . . . . . . 12 |- (v = s -> (E.w e. B (r C_ w /\ w C_ v) <-> E.w e. B (r C_ w /\ w C_ s)))
49	45, 48	3anbi23d 1171	. . . . . . . . . . 11 |- (v = s -> ((r e. c /\ v e. c /\ E.w e. B (r C_ w /\ w C_ v)) <-> (r e. c /\ s e. c /\ E.w e. B (r C_ w /\ w C_ s))))
50	38, 39, 44, 49	opelopab 3570	. . . . . . . . . 10 |- (<.r, s>. e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} <-> (r e. c /\ s e. c /\ E.w e. B (r C_ w /\ w C_ s)))
51		opelxpi 4040	. . . . . . . . . . 11 |- ((r e. c /\ s e. c) -> <.r, s>. e. (c X. c))
52	51	3adant3 896	. . . . . . . . . 10 |- ((r e. c /\ s e. c /\ E.w e. B (r C_ w /\ w C_ s)) -> <.r, s>. e. (c X. c))
53	50, 52	sylbi 216	. . . . . . . . 9 |- (<.r, s>. e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} -> <.r, s>. e. (c X. c))
54	37, 53	relssi 4078	. . . . . . . 8 |- {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} C_ (c X. c)
55	36, 54	ssexi 3456	. . . . . . 7 |- {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} e. _V
56		sseq2 2639	. . . . . . . 8 |- (y = (f` x) -> ((1st` x) C_ y <-> (1st` x) C_ (f` x)))
57		sseq1 2637	. . . . . . . 8 |- (y = (f` x) -> (y C_ (2nd` x) <-> (f` x) C_ (2nd` x)))
58	56, 57	anbi12d 690	. . . . . . 7 |- (y = (f` x) -> (((1st` x) C_ y /\ y C_ (2nd` x)) <-> ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))))
59	55, 58	ac6s 5918	. . . . . 6 |- (A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}E.y e. B ((1st` x) C_ y /\ y C_ (2nd` x)) -> E.f(f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))))
60	34, 59	syl 12	. . . . 5 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> E.f(f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))))
61		2ndctop 15474	. . . . . . . . . . 11 |- (J e. 2ndc -> J e. Top)
62	61	adantl 424	. . . . . . . . . 10 |- ((B e. Bases /\ J e. 2ndc) -> J e. Top)
63	62	ad2antrr 440	. . . . . . . . 9 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> J e. Top)
64		frn 4569	. . . . . . . . . . 11 |- (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B -> ran f C_ B)
65	64	ad2antrl 442	. . . . . . . . . 10 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> ran f C_ B)
66		bastg 8892	. . . . . . . . . . . . 13 |- (B e. Bases -> B C_ (topGen` B))
67	66	adantr 425	. . . . . . . . . . . 12 |- ((B e. Bases /\ J e. 2ndc) -> B C_ (topGen` B))
68	67	ad2antrr 440	. . . . . . . . . . 11 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> B C_ (topGen` B))
69		2ndcctbss.2	. . . . . . . . . . 11 |- J = (topGen` B)
70	68, 69	syl6ssr 2664	. . . . . . . . . 10 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> B C_ J)
71	65, 70	sstrd 2627	. . . . . . . . 9 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> ran f C_ J)
72		simplrl 454	. . . . . . . . . . . . 13 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> c e. Bases)
73		simprrl 458	. . . . . . . . . . . . . 14 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> o e. J)
74		simprr 451	. . . . . . . . . . . . . . 15 |- ((c e. Bases /\ (c ~<_ om /\ (topGen` c) = J)) -> (topGen` c) = J)
75	74	ad2antlr 441	. . . . . . . . . . . . . 14 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> (topGen` c) = J)
76	73, 75	eleqtrrd 1974	. . . . . . . . . . . . 13 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> o e. (topGen` c))
77		simprrr 459	. . . . . . . . . . . . 13 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> t e. o)
78		tg2 8891	. . . . . . . . . . . . 13 |- ((c e. Bases /\ o e. (topGen` c) /\ t e. o) -> E.d e. c (t e. d /\ d C_ o))
79	72, 76, 77, 78	syl111anc 1100	. . . . . . . . . . . 12 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> E.d e. c (t e. d /\ d C_ o))
80		simpll 448	. . . . . . . . . . . . . . . . 17 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> B e. Bases)
81	80	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> B e. Bases)
82		bastg 8892	. . . . . . . . . . . . . . . . . . . 20 |- (c e. Bases -> c C_ (topGen` c))
83	82	ad2antrl 442	. . . . . . . . . . . . . . . . . . 19 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> c C_ (topGen` c))
84	83	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> c C_ (topGen` c))
85	69	eqeq2i 1894	. . . . . . . . . . . . . . . . . . . . . 22 |- ((topGen` c) = J <-> (topGen` c) = (topGen` B))
86	85	biimpi 168	. . . . . . . . . . . . . . . . . . . . 21 |- ((topGen` c) = J -> (topGen` c) = (topGen` B))
87	86	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((c ~<_ om /\ (topGen` c) = J) -> (topGen` c) = (topGen` B))
88	87	ad2antll 443	. . . . . . . . . . . . . . . . . . 19 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> (topGen` c) = (topGen` B))
89	88	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> (topGen` c) = (topGen` B))
90	84, 89	sseqtrd 2653	. . . . . . . . . . . . . . . . 17 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> c C_ (topGen` B))
91		simprl 450	. . . . . . . . . . . . . . . . 17 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> d e. c)
92	90, 91	sseldd 2620	. . . . . . . . . . . . . . . 16 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> d e. (topGen` B))
93		simprrl 458	. . . . . . . . . . . . . . . 16 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> t e. d)
94		tg2 8891	. . . . . . . . . . . . . . . 16 |- ((B e. Bases /\ d e. (topGen` B) /\ t e. d) -> E.m e. B (t e. m /\ m C_ d))
95	81, 92, 93, 94	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> E.m e. B (t e. m /\ m C_ d))
96	72	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> c e. Bases)
97	67	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> B C_ (topGen` B))
98	97	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> B C_ (topGen` B))
99	75	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> (topGen` c) = J)
100	99, 69	syl6req 1945	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> (topGen` B) = (topGen` c))
101	98, 100	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . 20 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> B C_ (topGen` c))
102		simprl 450	. . . . . . . . . . . . . . . . . . . 20 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> m e. B)
103	101, 102	sseldd 2620	. . . . . . . . . . . . . . . . . . 19 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> m e. (topGen` c))
104		simprrl 458	. . . . . . . . . . . . . . . . . . 19 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> t e. m)
105		tg2 8891	. . . . . . . . . . . . . . . . . . 19 |- ((c e. Bases /\ m e. (topGen` c) /\ t e. m) -> E.n e. c (t e. n /\ n C_ m))
106	96, 103, 104, 105	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> E.n e. c (t e. n /\ n C_ m))
107		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B -> f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
108	107	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o)) -> f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
109	108	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
110	109	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
111		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> n e. c)
112	91	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> d e. c)
113		simplrl 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> m e. B)
114		simprrr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> n C_ m)
115		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. B /\ (t e. m /\ m C_ d)) -> m C_ d)
116	115	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> m C_ d)
117		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = m -> (n C_ w <-> n C_ m))
118		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = m -> (w C_ d <-> m C_ d))
119	117, 118	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = m -> ((n C_ w /\ w C_ d) <-> (n C_ m /\ m C_ d)))
120	119	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. B /\ (n C_ m /\ m C_ d)) -> E.w e. B (n C_ w /\ w C_ d))
121	113, 114, 116, 120	syl12anc 1098	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> E.w e. B (n C_ w /\ w C_ d))
122	111, 112, 121	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (n e. c /\ d e. c /\ E.w e. B (n C_ w /\ w C_ d)))
123		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- n e. _V
124		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- d e. _V
125		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u = n -> (u e. c <-> n e. c))
126		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (u = n -> (u C_ w <-> n C_ w))
127	126	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (u = n -> ((u C_ w /\ w C_ v) <-> (n C_ w /\ w C_ v)))
128	127	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u = n -> (E.w e. B (u C_ w /\ w C_ v) <-> E.w e. B (n C_ w /\ w C_ v)))
129	125, 128	3anbi13d 1170	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = n -> ((u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v)) <-> (n e. c /\ v e. c /\ E.w e. B (n C_ w /\ w C_ v))))
130		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = d -> (v e. c <-> d e. c))
131		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v = d -> (w C_ v <-> w C_ d))
132	131	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v = d -> ((n C_ w /\ w C_ v) <-> (n C_ w /\ w C_ d)))
133	132	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = d -> (E.w e. B (n C_ w /\ w C_ v) <-> E.w e. B (n C_ w /\ w C_ d)))
134	130, 133	3anbi23d 1171	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v = d -> ((n e. c /\ v e. c /\ E.w e. B (n C_ w /\ w C_ v)) <-> (n e. c /\ d e. c /\ E.w e. B (n C_ w /\ w C_ d))))
135	123, 124, 129, 134	opelopab 3570	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<.n, d>. e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} <-> (n e. c /\ d e. c /\ E.w e. B (n C_ w /\ w C_ d)))
136	122, 135	sylibr 217	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> <.n, d>. e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
137		fnfvelrn 4786	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} /\ <.n, d>. e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}) -> (f` <.n, d>.) e. ran f)
138	110, 136, 137	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (f` <.n, d>.) e. ran f)
139		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> n e. c)
140		simplll 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> d e. c)
141		simplrl 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> m e. B)
142		simprrr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> n C_ m)
143	115	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> m C_ d)
144	141, 142, 143, 120	syl12anc 1098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> E.w e. B (n C_ w /\ w C_ d))
145	139, 140, 144	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (n e. c /\ d e. c /\ E.w e. B (n C_ w /\ w C_ d)))
146	145, 135	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> <.n, d>. e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
147		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x = <.n, d>. -> (1st` x) = (1st` <.n, d>.))
148		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x = <.n, d>. -> (f` x) = (f` <.n, d>.))
149	147, 148	sseq12d 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = <.n, d>. -> ((1st` x) C_ (f` x) <-> (1st` <.n, d>.) C_ (f` <.n, d>.)))
150		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x = <.n, d>. -> (2nd` x) = (2nd` <.n, d>.))
151	148, 150	sseq12d 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = <.n, d>. -> ((f` x) C_ (2nd` x) <-> (f` <.n, d>.) C_ (2nd` <.n, d>.)))
152	149, 151	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = <.n, d>. -> (((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)) <-> ((1st` <.n, d>.) C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ (2nd` <.n, d>.))))
153	152	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<.n, d>. e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} -> (A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)) -> ((1st` <.n, d>.) C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ (2nd` <.n, d>.))))
154	146, 153	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)) -> ((1st` <.n, d>.) C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ (2nd` <.n, d>.))))
155		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) /\ (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d)) -> n C_ (f` <.n, d>.))
156		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((n e. c /\ (t e. n /\ n C_ m)) -> t e. n)
157	156	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) /\ (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d)) -> t e. n)
158	155, 157	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) /\ (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d)) -> t e. (f` <.n, d>.))
159		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) /\ (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d)) -> (f` <.n, d>.) C_ d)
160		simplrr 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) -> d C_ o)
161	160	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) /\ (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d)) -> d C_ o)
162	159, 161	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) /\ (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d)) -> (f` <.n, d>.) C_ o)
163	158, 162	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) /\ (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d)) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o))
164	163	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> ((n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))
165	123	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (1st` <.n, d>.) = n
166	165	sseq1i 2641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((1st` <.n, d>.) C_ (f` <.n, d>.) <-> n C_ (f` <.n, d>.))
167	123, 124	op2nd 5027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (2nd` <.n, d>.) = d
168	167	sseq2i 2642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f` <.n, d>.) C_ (2nd` <.n, d>.) <-> (f` <.n, d>.) C_ d)
169	166, 168	anbi12i 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((1st` <.n, d>.) C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ (2nd` <.n, d>.)) <-> (n C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ d))
170	164, 169	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (((1st` <.n, d>.) C_ (f` <.n, d>.) /\ (f` <.n, d>.) C_ (2nd` <.n, d>.)) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))
171	154, 170	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))
172	171	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)) -> ((((d e. c /\ (t e. d /\ d C_ o)) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))
173	172	exp4c 411	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)) -> ((d e. c /\ (t e. d /\ d C_ o)) -> ((m e. B /\ (t e. m /\ m C_ d)) -> ((n e. c /\ (t e. n /\ n C_ m)) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))))
174	173	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o)) -> ((d e. c /\ (t e. d /\ d C_ o)) -> ((m e. B /\ (t e. m /\ m C_ d)) -> ((n e. c /\ (t e. n /\ n C_ m)) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))))
175	174	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> ((d e. c /\ (t e. d /\ d C_ o)) -> ((m e. B /\ (t e. m /\ m C_ d)) -> ((n e. c /\ (t e. n /\ n C_ m)) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))))
176	175	imp41 395	. . . . . . . . . . . . . . . . . . . . 21 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o))
177		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b = (f` <.n, d>.) -> (t e. b <-> t e. (f` <.n, d>.)))
178		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b = (f` <.n, d>.) -> (b C_ o <-> (f` <.n, d>.) C_ o))
179	177, 178	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . 22 |- (b = (f` <.n, d>.) -> ((t e. b /\ b C_ o) <-> (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)))
180	179	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` <.n, d>.) e. ran f /\ (t e. (f` <.n, d>.) /\ (f` <.n, d>.) C_ o)) -> E.b e. ran f(t e. b /\ b C_ o))
181	138, 176, 180	syl11anc 524	. . . . . . . . . . . . . . . . . . . 20 |- (((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) /\ (n e. c /\ (t e. n /\ n C_ m))) -> E.b e. ran f(t e. b /\ b C_ o))
182	181	exp32 408	. . . . . . . . . . . . . . . . . . 19 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> (n e. c -> ((t e. n /\ n C_ m) -> E.b e. ran f(t e. b /\ b C_ o))))
183	182	r19.23adv 2215	. . . . . . . . . . . . . . . . . 18 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> (E.n e. c (t e. n /\ n C_ m) -> E.b e. ran f(t e. b /\ b C_ o)))
184	106, 183	mpd 29	. . . . . . . . . . . . . . . . 17 |- ((((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) /\ (m e. B /\ (t e. m /\ m C_ d))) -> E.b e. ran f(t e. b /\ b C_ o))
185	184	exp32 408	. . . . . . . . . . . . . . . 16 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> (m e. B -> ((t e. m /\ m C_ d) -> E.b e. ran f(t e. b /\ b C_ o))))
186	185	r19.23adv 2215	. . . . . . . . . . . . . . 15 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> (E.m e. B (t e. m /\ m C_ d) -> E.b e. ran f(t e. b /\ b C_ o)))
187	95, 186	mpd 29	. . . . . . . . . . . . . 14 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) /\ (d e. c /\ (t e. d /\ d C_ o))) -> E.b e. ran f(t e. b /\ b C_ o))
188	187	exp32 408	. . . . . . . . . . . . 13 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> (d e. c -> ((t e. d /\ d C_ o) -> E.b e. ran f(t e. b /\ b C_ o))))
189	188	r19.23adv 2215	. . . . . . . . . . . 12 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> (E.d e. c (t e. d /\ d C_ o) -> E.b e. ran f(t e. b /\ b C_ o)))
190	79, 189	mpd 29	. . . . . . . . . . 11 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) /\ (o e. J /\ t e. o))) -> E.b e. ran f(t e. b /\ b C_ o))
191	190	expr 418	. . . . . . . . . 10 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> ((o e. J /\ t e. o) -> E.b e. ran f(t e. b /\ b C_ o)))
192	191	r19.21aivv 2183	. . . . . . . . 9 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> A.o e. J A.t e. o E.b e. ran f(t e. b /\ b C_ o))
193		basgen2 8909	. . . . . . . . 9 |- ((J e. Top /\ ran f C_ J /\ A.o e. J A.t e. o E.b e. ran f(t e. b /\ b C_ o)) -> (ran f e. Bases /\ (topGen` ran f) = J))
194	63, 71, 192, 193	syl111anc 1100	. . . . . . . 8 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> (ran f e. Bases /\ (topGen` ran f) = J))
195		simprl 450	. . . . . . . . 9 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> ran f e. Bases)
196	107	adantr 425	. . . . . . . . . . . . 13 |- ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) -> f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
197	196	ad2antlr 441	. . . . . . . . . . . 12 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
198		dffn4 4623	. . . . . . . . . . . 12 |- (f Fn {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} <-> f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-onto->ran f)
199	197, 198	sylib 215	. . . . . . . . . . 11 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-onto->ran f)
200	55	fodom 5960	. . . . . . . . . . 11 |- (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-onto->ran f -> ran f ~<_ {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
201	199, 200	syl 12	. . . . . . . . . 10 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> ran f ~<_ {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))})
202		omex 5733	. . . . . . . . . . . . . . . . 17 |- om e. _V
203	202, 35	xpdom1 5502	. . . . . . . . . . . . . . . 16 |- (c ~<_ om -> (c X. c) ~<_ (om X. c))
204	202, 202	xpdom2 5501	. . . . . . . . . . . . . . . 16 |- (c ~<_ om -> (om X. c) ~<_ (om X. om))
205		domtr 5474	. . . . . . . . . . . . . . . 16 |- (((c X. c) ~<_ (om X. c) /\ (om X. c) ~<_ (om X. om)) -> (c X. c) ~<_ (om X. om))
206	203, 204, 205	syl11anc 524	. . . . . . . . . . . . . . 15 |- (c ~<_ om -> (c X. c) ~<_ (om X. om))
207		xpomen 8769	. . . . . . . . . . . . . . . 16 |- (om X. om) ~~ om
208		domentr 5480	. . . . . . . . . . . . . . . 16 |- (((c X. c) ~<_ (om X. om) /\ (om X. om) ~~ om) -> (c X. c) ~<_ om)
209	207, 208	mpan2 760	. . . . . . . . . . . . . . 15 |- ((c X. c) ~<_ (om X. om) -> (c X. c) ~<_ om)
210	206, 209	syl 12	. . . . . . . . . . . . . 14 |- (c ~<_ om -> (c X. c) ~<_ om)
211	210	adantr 425	. . . . . . . . . . . . 13 |- ((c ~<_ om /\ (topGen` c) = J) -> (c X. c) ~<_ om)
212	211	ad2antll 443	. . . . . . . . . . . 12 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> (c X. c) ~<_ om)
213	212	ad2antrr 440	. . . . . . . . . . 11 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> (c X. c) ~<_ om)
214		ssdomg 5467	. . . . . . . . . . . . 13 |- ({<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} e. _V -> ({<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} C_ (c X. c) -> {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ~<_ (c X. c)))
215	55, 54, 214	mp2 54	. . . . . . . . . . . 12 |- {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ~<_ (c X. c)
216		domtr 5474	. . . . . . . . . . . 12 |- (({<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ~<_ (c X. c) /\ (c X. c) ~<_ om) -> {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ~<_ om)
217	215, 216	mpan 759	. . . . . . . . . . 11 |- ((c X. c) ~<_ om -> {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ~<_ om)
218	213, 217	syl 12	. . . . . . . . . 10 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ~<_ om)
219		domtr 5474	. . . . . . . . . 10 |- ((ran f ~<_ {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} /\ {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ~<_ om) -> ran f ~<_ om)
220	201, 218, 219	syl11anc 524	. . . . . . . . 9 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> ran f ~<_ om)
221	65	adantr 425	. . . . . . . . 9 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> ran f C_ B)
222		simprr 451	. . . . . . . . . 10 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> (topGen` ran f) = J)
223	222	eqcomd 1889	. . . . . . . . 9 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> J = (topGen` ran f))
224		breq1 3341	. . . . . . . . . . 11 |- (b = ran f -> (b ~<_ om <-> ran f ~<_ om))
225		sseq1 2637	. . . . . . . . . . 11 |- (b = ran f -> (b C_ B <-> ran f C_ B))
226		fveq2 4681	. . . . . . . . . . . 12 |- (b = ran f -> (topGen` b) = (topGen` ran f))
227	226	eqeq2d 1895	. . . . . . . . . . 11 |- (b = ran f -> (J = (topGen` b) <-> J = (topGen` ran f)))
228	224, 225, 227	3anbi123d 1168	. . . . . . . . . 10 |- (b = ran f -> ((b ~<_ om /\ b C_ B /\ J = (topGen` b)) <-> (ran f ~<_ om /\ ran f C_ B /\ J = (topGen` ran f))))
229	228	rcla4ev 2381	. . . . . . . . 9 |- ((ran f e. Bases /\ (ran f ~<_ om /\ ran f C_ B /\ J = (topGen` ran f))) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b)))
230	195, 220, 221, 223, 229	syl13anc 1102	. . . . . . . 8 |- (((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) /\ (ran f e. Bases /\ (topGen` ran f) = J)) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b)))
231	194, 230	mpdan 768	. . . . . . 7 |- ((((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) /\ (f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x)))) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b)))
232	231	ex 402	. . . . . 6 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> ((f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b))))
233	232	19.23adv 1584	. . . . 5 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> (E.f(f:{<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))}-->B /\ A.x e. {<.u, v>. | (u e. c /\ v e. c /\ E.w e. B (u C_ w /\ w C_ v))} ((1st` x) C_ (f` x) /\ (f` x) C_ (2nd` x))) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b))))
234	60, 233	mpd 29	. . . 4 |- (((B e. Bases /\ J e. 2ndc) /\ (c e. Bases /\ (c ~<_ om /\ (topGen` c) = J))) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b)))
235	234	exp32 408	. . 3 |- ((B e. Bases /\ J e. 2ndc) -> (c e. Bases -> ((c ~<_ om /\ (topGen` c) = J) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b)))))
236	235	r19.23adv 2215	. 2 |- ((B e. Bases /\ J e. 2ndc) -> (E.c e. Bases (c ~<_ om /\ (topGen` c) = J) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b))))
237	2, 236	mpd 29	1 |- ((B e. Bases /\ J e. 2ndc) -> E.b e. Bases (b ~<_ om /\ b C_ B /\ J = (topGen` b)))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395  omcom 3949   X. cxp 3984  ran crn 3987   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998  1stc1st 5018  2ndc2nd 5019   ~~ cen 5423   ~<_ cdom 5424  Topctop 8857  Basesctb 8859  topGenctg 8860  2ndcc2ndc 15456

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  ax-inf2 5731  ax-ac 5906

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-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  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-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-r1 5750  df-rank 5751  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-seq1 7721  df-exp 7812  df-top 8861  df-bases 8863  df-topgen 8864  df-2ndc 15462

Copyright terms: Public domain