Theorem topjoin 15527

Description: Two equivalent formulations of the join of a collection of topologies.

Assertion

Ref	Expression
topjoin	|- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})

Distinct variable groups:   j,k,A   S,j,k   j,X,k

Proof of Theorem topjoin

Step	Hyp	Ref	Expression
1		iftrue 2989	. . . 4 |- (S = (/) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = {(/), X})
2	1	adantl 424	. . 3 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = {(/), X})
3		simpr 350	. . . . . . . . . . . 12 |- ((a e. Top /\ X = U.a) -> X = U.a)
4		uniexg 3795	. . . . . . . . . . . . 13 |- (a e. Top -> U.a e. _V)
5	4	adantr 425	. . . . . . . . . . . 12 |- ((a e. Top /\ X = U.a) -> U.a e. _V)
6	3, 5	eqeltrd 1971	. . . . . . . . . . 11 |- ((a e. Top /\ X = U.a) -> X e. _V)
7		0ex 3446	. . . . . . . . . . . 12 |- (/) e. _V
8		prssg 3140	. . . . . . . . . . . 12 |- (((/) e. _V /\ X e. _V) -> (((/) e. a /\ X e. a) <-> {(/), X} C_ a))
9	7, 8	mpan 759	. . . . . . . . . . 11 |- (X e. _V -> (((/) e. a /\ X e. a) <-> {(/), X} C_ a))
10	6, 9	syl 12	. . . . . . . . . 10 |- ((a e. Top /\ X = U.a) -> (((/) e. a /\ X e. a) <-> {(/), X} C_ a))
11		0opn 8870	. . . . . . . . . . 11 |- (a e. Top -> (/) e. a)
12	11	adantr 425	. . . . . . . . . 10 |- ((a e. Top /\ X = U.a) -> (/) e. a)
13		eqid 1884	. . . . . . . . . . . . 13 |- U.a = U.a
14	13	topopn 8871	. . . . . . . . . . . 12 |- (a e. Top -> U.a e. a)
15	14	adantr 425	. . . . . . . . . . 11 |- ((a e. Top /\ X = U.a) -> U.a e. a)
16	3, 15	eqeltrd 1971	. . . . . . . . . 10 |- ((a e. Top /\ X = U.a) -> X e. a)
17	10, 12, 16	mpbi2and 801	. . . . . . . . 9 |- ((a e. Top /\ X = U.a) -> {(/), X} C_ a)
18	17	adantrr 431	. . . . . . . 8 |- ((a e. Top /\ (X = U.a /\ A.j e. S j C_ a)) -> {(/), X} C_ a)
19	18	a1i 8	. . . . . . 7 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> ((a e. Top /\ (X = U.a /\ A.j e. S j C_ a)) -> {(/), X} C_ a))
20		unieq 3185	. . . . . . . . . 10 |- (k = a -> U.k = U.a)
21	20	eqeq2d 1895	. . . . . . . . 9 |- (k = a -> (X = U.k <-> X = U.a))
22		sseq2 2639	. . . . . . . . . 10 |- (k = a -> (j C_ k <-> j C_ a))
23	22	ralbidv 2123	. . . . . . . . 9 |- (k = a -> (A.j e. S j C_ k <-> A.j e. S j C_ a))
24	21, 23	anbi12d 690	. . . . . . . 8 |- (k = a -> ((X = U.k /\ A.j e. S j C_ k) <-> (X = U.a /\ A.j e. S j C_ a)))
25	24	elrab 2414	. . . . . . 7 |- (a e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} <-> (a e. Top /\ (X = U.a /\ A.j e. S j C_ a)))
26	19, 25	syl5ib 223	. . . . . 6 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> (a e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} -> {(/), X} C_ a))
27	26	r19.21aiv 2175	. . . . 5 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> A.a e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)}{(/), X} C_ a)
28		ssint 3232	. . . . 5 |- ({(/), X} C_ |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)} <-> A.a e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)}{(/), X} C_ a)
29	27, 28	sylibr 217	. . . 4 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> {(/), X} C_ |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})
30		uniprg 3192	. . . . . . . . . . 11 |- (((/) e. _V /\ X e. A) -> U.{(/), X} = ((/) u. X))
31	7, 30	mpan 759	. . . . . . . . . 10 |- (X e. A -> U.{(/), X} = ((/) u. X))
32		un0 2896	. . . . . . . . . . 11 |- (X u. (/)) = X
33		uncom 2744	. . . . . . . . . . 11 |- (X u. (/)) = ((/) u. X)
34	32, 33	eqtr3i 1910	. . . . . . . . . 10 |- X = ((/) u. X)
35	31, 34	syl6reqr 1947	. . . . . . . . 9 |- (X e. A -> X = U.{(/), X})
36	35	ad2antrr 440	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> X = U.{(/), X})
37		ral0 2974	. . . . . . . . . 10 |- A.j e. (/) j C_ {(/), X}
38		raleq 2266	. . . . . . . . . 10 |- (S = (/) -> (A.j e. S j C_ {(/), X} <-> A.j e. (/) j C_ {(/), X}))
39	37, 38	mpbiri 211	. . . . . . . . 9 |- (S = (/) -> A.j e. S j C_ {(/), X})
40	39	adantl 424	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> A.j e. S j C_ {(/), X})
41	36, 40	jca 310	. . . . . . 7 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> (X = U.{(/), X} /\ A.j e. S j C_ {(/), X}))
42		indistop 8918	. . . . . . 7 |- {(/), X} e. Top
43	41, 42	jctil 316	. . . . . 6 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> ({(/), X} e. Top /\ (X = U.{(/), X} /\ A.j e. S j C_ {(/), X})))
44		unieq 3185	. . . . . . . . 9 |- (k = {(/), X} -> U.k = U.{(/), X})
45	44	eqeq2d 1895	. . . . . . . 8 |- (k = {(/), X} -> (X = U.k <-> X = U.{(/), X}))
46		sseq2 2639	. . . . . . . . 9 |- (k = {(/), X} -> (j C_ k <-> j C_ {(/), X}))
47	46	ralbidv 2123	. . . . . . . 8 |- (k = {(/), X} -> (A.j e. S j C_ k <-> A.j e. S j C_ {(/), X}))
48	45, 47	anbi12d 690	. . . . . . 7 |- (k = {(/), X} -> ((X = U.k /\ A.j e. S j C_ k) <-> (X = U.{(/), X} /\ A.j e. S j C_ {(/), X})))
49	48	elrab 2414	. . . . . 6 |- ({(/), X} e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} <-> ({(/), X} e. Top /\ (X = U.{(/), X} /\ A.j e. S j C_ {(/), X})))
50	43, 49	sylibr 217	. . . . 5 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> {(/), X} e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)})
51		intss1 3231	. . . . 5 |- ({(/), X} e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} -> |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)} C_ {(/), X})
52	50, 51	syl 12	. . . 4 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)} C_ {(/), X})
53	29, 52	eqssd 2633	. . 3 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> {(/), X} = |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})
54	2, 53	eqtrd 1925	. 2 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ S = (/)) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})
55		iffalse 2991	. . . 4 |- (-. S = (/) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = (topGen` ( fi ` U.S)))
56	55	adantl 424	. . 3 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = (topGen` ( fi ` U.S)))
57		ssexg 3457	. . . . . . . . . . . . . . . 16 |- ((S C_ {j e. Top | X = U.j} /\ {j e. Top | X = U.j} e. _V) -> S e. _V)
58		pwexg 3489	. . . . . . . . . . . . . . . . 17 |- (X e. A -> ~PX e. _V)
59		pwexg 3489	. . . . . . . . . . . . . . . . . 18 |- (~PX e. _V -> ~P~PX e. _V)
60		df-pw 3035	. . . . . . . . . . . . . . . . . 18 |- ~P~PX = {j | j C_ ~PX}
61	59, 60	syl5eqelr 1976	. . . . . . . . . . . . . . . . 17 |- (~PX e. _V -> {j | j C_ ~PX} e. _V)
62		df-rab 2112	. . . . . . . . . . . . . . . . . . 19 |- {j e. Top | X = U.j} = {j | (j e. Top /\ X = U.j)}
63		pwuni 3505	. . . . . . . . . . . . . . . . . . . . . . 23 |- j C_ ~PU.j
64	63	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (X = U.j -> j C_ ~PU.j)
65		pweq 3036	. . . . . . . . . . . . . . . . . . . . . 22 |- (X = U.j -> ~PX = ~PU.j)
66	64, 65	sseqtr4d 2654	. . . . . . . . . . . . . . . . . . . . 21 |- (X = U.j -> j C_ ~PX)
67	66	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((j e. Top /\ X = U.j) -> j C_ ~PX)
68	67	ss2abi 2679	. . . . . . . . . . . . . . . . . . 19 |- {j | (j e. Top /\ X = U.j)} C_ {j | j C_ ~PX}
69	62, 68	eqsstri 2647	. . . . . . . . . . . . . . . . . 18 |- {j e. Top | X = U.j} C_ {j | j C_ ~PX}
70		ssexg 3457	. . . . . . . . . . . . . . . . . 18 |- (({j e. Top | X = U.j} C_ {j | j C_ ~PX} /\ {j | j C_ ~PX} e. _V) -> {j e. Top | X = U.j} e. _V)
71	69, 70	mpan 759	. . . . . . . . . . . . . . . . 17 |- ({j | j C_ ~PX} e. _V -> {j e. Top | X = U.j} e. _V)
72	58, 61, 71	3syl 24	. . . . . . . . . . . . . . . 16 |- (X e. A -> {j e. Top | X = U.j} e. _V)
73	57, 72	sylan2 500	. . . . . . . . . . . . . . 15 |- ((S C_ {j e. Top | X = U.j} /\ X e. A) -> S e. _V)
74	73	ancoms 484	. . . . . . . . . . . . . 14 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> S e. _V)
75	74	adantr 425	. . . . . . . . . . . . 13 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> S e. _V)
76		uniexg 3795	. . . . . . . . . . . . 13 |- (S e. _V -> U.S e. _V)
77	75, 76	syl 12	. . . . . . . . . . . 12 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> U.S e. _V)
78	77	adantr 425	. . . . . . . . . . 11 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> U.S e. _V)
79		fibas 10221	. . . . . . . . . . 11 |- (U.S e. _V -> ( fi ` U.S) e. Bases)
80	78, 79	syl 12	. . . . . . . . . 10 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> ( fi ` U.S) e. Bases)
81		topbas 8897	. . . . . . . . . . 11 |- (t e. Top -> t e. Bases)
82	81	ad2antrl 442	. . . . . . . . . 10 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> t e. Bases)
83		simprl 450	. . . . . . . . . . . 12 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> t e. Top)
84		unissb 3208	. . . . . . . . . . . . . . 15 |- (U.S C_ t <-> A.j e. S j C_ t)
85	84	biimpri 169	. . . . . . . . . . . . . 14 |- (A.j e. S j C_ t -> U.S C_ t)
86	85	adantl 424	. . . . . . . . . . . . 13 |- ((X = U.t /\ A.j e. S j C_ t) -> U.S C_ t)
87	86	ad2antll 443	. . . . . . . . . . . 12 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> U.S C_ t)
88		fiss 15368	. . . . . . . . . . . 12 |- ((t e. Top /\ U.S C_ t) -> ( fi ` U.S) C_ ( fi ` t))
89	83, 87, 88	syl11anc 524	. . . . . . . . . . 11 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> ( fi ` U.S) C_ ( fi ` t))
90		fitop 15401	. . . . . . . . . . . 12 |- (t e. Top -> ( fi ` t) = t)
91	90	ad2antrl 442	. . . . . . . . . . 11 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> ( fi ` t) = t)
92	89, 91	sseqtrd 2653	. . . . . . . . . 10 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> ( fi ` U.S) C_ t)
93		tgss 8906	. . . . . . . . . 10 |- ((( fi ` U.S) e. Bases /\ t e. Bases /\ ( fi ` U.S) C_ t) -> (topGen` ( fi ` U.S)) C_ (topGen` t))
94	80, 82, 92, 93	syl111anc 1100	. . . . . . . . 9 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> (topGen` ( fi ` U.S)) C_ (topGen` t))
95		tgtop 8898	. . . . . . . . . 10 |- (t e. Top -> (topGen` t) = t)
96	95	ad2antrl 442	. . . . . . . . 9 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> (topGen` t) = t)
97	94, 96	sseqtrd 2653	. . . . . . . 8 |- ((((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) /\ (t e. Top /\ (X = U.t /\ A.j e. S j C_ t))) -> (topGen` ( fi ` U.S)) C_ t)
98	97	ex 402	. . . . . . 7 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> ((t e. Top /\ (X = U.t /\ A.j e. S j C_ t)) -> (topGen` ( fi ` U.S)) C_ t))
99		unieq 3185	. . . . . . . . . 10 |- (k = t -> U.k = U.t)
100	99	eqeq2d 1895	. . . . . . . . 9 |- (k = t -> (X = U.k <-> X = U.t))
101		sseq2 2639	. . . . . . . . . 10 |- (k = t -> (j C_ k <-> j C_ t))
102	101	ralbidv 2123	. . . . . . . . 9 |- (k = t -> (A.j e. S j C_ k <-> A.j e. S j C_ t))
103	100, 102	anbi12d 690	. . . . . . . 8 |- (k = t -> ((X = U.k /\ A.j e. S j C_ k) <-> (X = U.t /\ A.j e. S j C_ t)))
104	103	elrab 2414	. . . . . . 7 |- (t e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} <-> (t e. Top /\ (X = U.t /\ A.j e. S j C_ t)))
105	98, 104	syl5ib 223	. . . . . 6 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (t e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} -> (topGen` ( fi ` U.S)) C_ t))
106	105	r19.21aiv 2175	. . . . 5 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> A.t e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} (topGen` ( fi ` U.S)) C_ t)
107		ssint 3232	. . . . 5 |- ((topGen` ( fi ` U.S)) C_ |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)} <-> A.t e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} (topGen` ( fi ` U.S)) C_ t)
108	106, 107	sylibr 217	. . . 4 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (topGen` ( fi ` U.S)) C_ |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})
109		simpr 350	. . . . . . . . . . 11 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> S C_ {j e. Top | X = U.j})
110	72	adantr 425	. . . . . . . . . . 11 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> {j e. Top | X = U.j} e. _V)
111	109, 110, 57	syl11anc 524	. . . . . . . . . 10 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> S e. _V)
112	111, 76, 79	3syl 24	. . . . . . . . 9 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> ( fi ` U.S) e. Bases)
113	112	adantr 425	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> ( fi ` U.S) e. Bases)
114		tgcl 8894	. . . . . . . 8 |- (( fi ` U.S) e. Bases -> (topGen` ( fi ` U.S)) e. Top)
115	113, 114	syl 12	. . . . . . 7 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (topGen` ( fi ` U.S)) e. Top)
116		fiuni 10219	. . . . . . . . 9 |- (U.S e. _V -> U.U.S = U.( fi ` U.S))
117	75, 76, 116	3syl 24	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> U.U.S = U.( fi ` U.S))
118		ssel2 2616	. . . . . . . . . . . . . . . . 17 |- ((S C_ {j e. Top | X = U.j} /\ t e. S) -> t e. {j e. Top | X = U.j})
119	118	adantll 428	. . . . . . . . . . . . . . . 16 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ t e. S) -> t e. {j e. Top | X = U.j})
120		simpr 350	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. Top /\ X = U.t) -> X = U.t)
121		eqid 1884	. . . . . . . . . . . . . . . . . . . . . 22 |- U.t = U.t
122	121	topopn 8871	. . . . . . . . . . . . . . . . . . . . 21 |- (t e. Top -> U.t e. t)
123	122	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. Top /\ X = U.t) -> U.t e. t)
124	120, 123	eqeltrd 1971	. . . . . . . . . . . . . . . . . . 19 |- ((t e. Top /\ X = U.t) -> X e. t)
125	124	adantl 424	. . . . . . . . . . . . . . . . . 18 |- ((X e. A /\ (t e. Top /\ X = U.t)) -> X e. t)
126		unieq 3185	. . . . . . . . . . . . . . . . . . . 20 |- (j = t -> U.j = U.t)
127	126	eqeq2d 1895	. . . . . . . . . . . . . . . . . . 19 |- (j = t -> (X = U.j <-> X = U.t))
128	127	elrab 2414	. . . . . . . . . . . . . . . . . 18 |- (t e. {j e. Top | X = U.j} <-> (t e. Top /\ X = U.t))
129	125, 128	sylan2b 501	. . . . . . . . . . . . . . . . 17 |- ((X e. A /\ t e. {j e. Top | X = U.j}) -> X e. t)
130	129	adantlr 429	. . . . . . . . . . . . . . . 16 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ t e. {j e. Top | X = U.j}) -> X e. t)
131	119, 130	syldan 516	. . . . . . . . . . . . . . 15 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ t e. S) -> X e. t)
132		elunii 3182	. . . . . . . . . . . . . . 15 |- ((X e. t /\ t e. S) -> X e. U.S)
133	131, 132	sylancom 531	. . . . . . . . . . . . . 14 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ t e. S) -> X e. U.S)
134	133	ex 402	. . . . . . . . . . . . 13 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> (t e. S -> X e. U.S))
135	134	19.23adv 1584	. . . . . . . . . . . 12 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> (E.t t e. S -> X e. U.S))
136	135	imp 377	. . . . . . . . . . 11 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ E.t t e. S) -> X e. U.S)
137		df-ne 2019	. . . . . . . . . . . 12 |- (S =/= (/) <-> -. S = (/))
138		n0 2884	. . . . . . . . . . . 12 |- (S =/= (/) <-> E.t t e. S)
139	137, 138	bitr3i 192	. . . . . . . . . . 11 |- (-. S = (/) <-> E.t t e. S)
140	136, 139	sylan2b 501	. . . . . . . . . 10 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> X e. U.S)
141		elssuni 3206	. . . . . . . . . 10 |- (X e. U.S -> X C_ U.U.S)
142	140, 141	syl 12	. . . . . . . . 9 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> X C_ U.U.S)
143		ssel 2615	. . . . . . . . . . . . . . . . 17 |- (S C_ {j e. Top | X = U.j} -> (k e. S -> k e. {j e. Top | X = U.j}))
144		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . 23 |- U.k = U.k
145	144	eltopss 8872	. . . . . . . . . . . . . . . . . . . . . 22 |- ((k e. Top /\ t e. k) -> t C_ U.k)
146	145	adantlr 429	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Top /\ X = U.k) /\ t e. k) -> t C_ U.k)
147		simplr 449	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Top /\ X = U.k) /\ t e. k) -> X = U.k)
148	146, 147	sseqtr4d 2654	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. Top /\ X = U.k) /\ t e. k) -> t C_ X)
149	148	ex 402	. . . . . . . . . . . . . . . . . . 19 |- ((k e. Top /\ X = U.k) -> (t e. k -> t C_ X))
150	149	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (X e. A -> ((k e. Top /\ X = U.k) -> (t e. k -> t C_ X)))
151		unieq 3185	. . . . . . . . . . . . . . . . . . . 20 |- (j = k -> U.j = U.k)
152	151	eqeq2d 1895	. . . . . . . . . . . . . . . . . . 19 |- (j = k -> (X = U.j <-> X = U.k))
153	152	elrab 2414	. . . . . . . . . . . . . . . . . 18 |- (k e. {j e. Top | X = U.j} <-> (k e. Top /\ X = U.k))
154	150, 153	syl5ib 223	. . . . . . . . . . . . . . . . 17 |- (X e. A -> (k e. {j e. Top | X = U.j} -> (t e. k -> t C_ X)))
155	143, 154	syl9r 72	. . . . . . . . . . . . . . . 16 |- (X e. A -> (S C_ {j e. Top | X = U.j} -> (k e. S -> (t e. k -> t C_ X))))
156	155	com34 40	. . . . . . . . . . . . . . 15 |- (X e. A -> (S C_ {j e. Top | X = U.j} -> (t e. k -> (k e. S -> t C_ X))))
157	156	imp4b 392	. . . . . . . . . . . . . 14 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> ((t e. k /\ k e. S) -> t C_ X))
158	157	adantr 425	. . . . . . . . . . . . 13 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> ((t e. k /\ k e. S) -> t C_ X))
159	158	19.23adv 1584	. . . . . . . . . . . 12 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (E.k(t e. k /\ k e. S) -> t C_ X))
160		eluni 3180	. . . . . . . . . . . 12 |- (t e. U.S <-> E.k(t e. k /\ k e. S))
161	159, 160	syl5ib 223	. . . . . . . . . . 11 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (t e. U.S -> t C_ X))
162	161	r19.21aiv 2175	. . . . . . . . . 10 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> A.t e. U.St C_ X)
163		unissb 3208	. . . . . . . . . 10 |- (U.U.S C_ X <-> A.t e. U.St C_ X)
164	162, 163	sylibr 217	. . . . . . . . 9 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> U.U.S C_ X)
165	142, 164	eqssd 2633	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> X = U.U.S)
166		unitg 8893	. . . . . . . . 9 |- (( fi ` U.S) e. Bases -> U.(topGen` ( fi ` U.S)) = U.( fi ` U.S))
167	113, 166	syl 12	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> U.(topGen` ( fi ` U.S)) = U.( fi ` U.S))
168	117, 165, 167	3eqtr4d 1937	. . . . . . 7 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> X = U.(topGen` ( fi ` U.S)))
169		ax-17 1317	. . . . . . . . . 10 |- (X e. A -> A.j X e. A)
170		ax-17 1317	. . . . . . . . . . 11 |- (k e. S -> A.j k e. S)
171		hbrab1 2257	. . . . . . . . . . 11 |- (k e. {j e. Top | X = U.j} -> A.j k e. {j e. Top | X = U.j})
172	170, 171	hbss 2614	. . . . . . . . . 10 |- (S C_ {j e. Top | X = U.j} -> A.j S C_ {j e. Top | X = U.j})
173	169, 172	hban 1356	. . . . . . . . 9 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> A.j(X e. A /\ S C_ {j e. Top | X = U.j}))
174		ax-17 1317	. . . . . . . . 9 |- (-. S = (/) -> A.j -. S = (/))
175	173, 174	hban 1356	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> A.j((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)))
176		sstr2 2623	. . . . . . . . . 10 |- (j C_ U.S -> (U.S C_ (topGen` ( fi ` U.S)) -> j C_ (topGen` ( fi ` U.S))))
177		abfi2 10216	. . . . . . . . . . . . 13 |- (U.S e. _V -> U.S C_ ( fi ` U.S))
178	111, 76, 177	3syl 24	. . . . . . . . . . . 12 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> U.S C_ ( fi ` U.S))
179	111, 76	syl 12	. . . . . . . . . . . . 13 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> U.S e. _V)
180		bastg 8892	. . . . . . . . . . . . 13 |- (( fi ` U.S) e. Bases -> ( fi ` U.S) C_ (topGen` ( fi ` U.S)))
181	179, 79, 180	3syl 24	. . . . . . . . . . . 12 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> ( fi ` U.S) C_ (topGen` ( fi ` U.S)))
182	178, 181	sstrd 2627	. . . . . . . . . . 11 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> U.S C_ (topGen` ( fi ` U.S)))
183	182	adantr 425	. . . . . . . . . 10 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> U.S C_ (topGen` ( fi ` U.S)))
184	176, 183	syl5com 63	. . . . . . . . 9 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (j C_ U.S -> j C_ (topGen` ( fi ` U.S))))
185		elssuni 3206	. . . . . . . . 9 |- (j e. S -> j C_ U.S)
186	184, 185	syl5 20	. . . . . . . 8 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (j e. S -> j C_ (topGen` ( fi ` U.S))))
187	175, 186	r19.21ai 2174	. . . . . . 7 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> A.j e. S j C_ (topGen` ( fi ` U.S)))
188	115, 168, 187	jca32 312	. . . . . 6 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> ((topGen` ( fi ` U.S)) e. Top /\ (X = U.(topGen` ( fi ` U.S)) /\ A.j e. S j C_ (topGen` ( fi ` U.S)))))
189		unieq 3185	. . . . . . . . 9 |- (k = (topGen` ( fi ` U.S)) -> U.k = U.(topGen` ( fi ` U.S)))
190	189	eqeq2d 1895	. . . . . . . 8 |- (k = (topGen` ( fi ` U.S)) -> (X = U.k <-> X = U.(topGen` ( fi ` U.S))))
191		sseq2 2639	. . . . . . . . 9 |- (k = (topGen` ( fi ` U.S)) -> (j C_ k <-> j C_ (topGen` ( fi ` U.S))))
192	191	ralbidv 2123	. . . . . . . 8 |- (k = (topGen` ( fi ` U.S)) -> (A.j e. S j C_ k <-> A.j e. S j C_ (topGen` ( fi ` U.S))))
193	190, 192	anbi12d 690	. . . . . . 7 |- (k = (topGen` ( fi ` U.S)) -> ((X = U.k /\ A.j e. S j C_ k) <-> (X = U.(topGen` ( fi ` U.S)) /\ A.j e. S j C_ (topGen` ( fi ` U.S)))))
194	193	elrab 2414	. . . . . 6 |- ((topGen` ( fi ` U.S)) e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} <-> ((topGen` ( fi ` U.S)) e. Top /\ (X = U.(topGen` ( fi ` U.S)) /\ A.j e. S j C_ (topGen` ( fi ` U.S)))))
195	188, 194	sylibr 217	. . . . 5 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (topGen` ( fi ` U.S)) e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)})
196		intss1 3231	. . . . 5 |- ((topGen` ( fi ` U.S)) e. {k e. Top | (X = U.k /\ A.j e. S j C_ k)} -> |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)} C_ (topGen` ( fi ` U.S)))
197	195, 196	syl 12	. . . 4 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)} C_ (topGen` ( fi ` U.S)))
198	108, 197	eqssd 2633	. . 3 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> (topGen` ( fi ` U.S)) = |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})
199	56, 198	eqtrd 1925	. 2 |- (((X e. A /\ S C_ {j e. Top | X = U.j}) /\ -. S = (/)) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})
200	54, 199	pm2.61dan 535	1 |- ((X e. A /\ S C_ {j e. Top | X = U.j}) -> if(S = (/), {(/), X}, (topGen` ( fi ` U.S))) = |^|{k e. Top | (X = U.k /\ A.j e. S j C_ k)})

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  {crab 2108  _Vcvv 2292   u. cun 2591   C_ wss 2593  (/)c0 2875  ifcif 2982  ~Pcpw 3032  {cpr 3045  U.cuni 3177  |^|cint 3214  ` cfv 3998  Topctop 8857  Basesctb 8859  topGenctg 8860   fi cfi 10210

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

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-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-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-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-top 8861  df-bases 8863  df-topgen 8864  df-fi 10211

Copyright terms: Public domain