Theorem topjoin 28612

Description: Two equivalent formulations of the join of a collection of topologies. (Contributed by Jeff Hankins, 6-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

Assertion

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

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

Proof of Theorem topjoin

Step	Hyp	Ref	Expression
1		topontop 18553	. . . . . . 7 |- ( k e. (TopOn ` X ) -> k e. Top )
2	1	ad2antrl 727	. . . . . 6 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> k e. Top )
3		toponmax 18555	. . . . . . . . 9 |- ( k e. (TopOn ` X ) -> X e. k )
4	3	ad2antrl 727	. . . . . . . 8 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> X e. k )
5	4	snssd 4039	. . . . . . 7 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> { X } C_ k )
6		simprr 756	. . . . . . . 8 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> A. j e. S j C_ k )
7		unissb 4144	. . . . . . . 8 |- ( U. S C_ k <-> A. j e. S j C_ k )
8	6, 7	sylibr 212	. . . . . . 7 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> U. S C_ k )
9	5, 8	unssd 3553	. . . . . 6 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> ( { X } u. U. S ) C_ k )
10		tgfiss 18618	. . . . . 6 |- ( ( k e. Top /\ ( { X } u. U. S ) C_ k ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ k )
11	2, 9, 10	syl2anc 661	. . . . 5 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ k )
12	11	expr 615	. . . 4 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ k e. (TopOn ` X ) ) -> ( A. j e. S j C_ k -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ k ) )
13	12	ralrimiva 2820	. . 3 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> A. k e. (TopOn ` X ) ( A. j e. S j C_ k -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ k ) )
14		ssintrab 4172	. . 3 |- ( ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ |^| { k e. (TopOn ` X ) | A. j e. S j C_ k } <-> A. k e. (TopOn ` X ) ( A. j e. S j C_ k -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ k ) )
15	13, 14	sylibr 212	. 2 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ |^| { k e. (TopOn ` X ) | A. j e. S j C_ k } )
16		fibas 18604	. . . . . 6 |- ( fi ` ( { X } u. U. S ) ) e. TopBases
17		tgtopon 18598	. . . . . 6 |- ( ( fi ` ( { X } u. U. S ) ) e. TopBases -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. (TopOn ` U. ( fi ` ( { X } u. U. S ) ) ) )
18	16, 17	ax-mp 5	. . . . 5 |- ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. (TopOn ` U. ( fi ` ( { X } u. U. S ) ) )
19		uniun 4131	. . . . . . . 8 |- U. ( { X } u. U. S ) = ( U. { X } u. U. U. S )
20		unisng 4128	. . . . . . . . . 10 |- ( X e. V -> U. { X } = X )
21	20	adantr 465	. . . . . . . . 9 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. { X } = X )
22	21	uneq1d 3530	. . . . . . . 8 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( U. { X } u. U. U. S ) = ( X u. U. U. S ) )
23	19, 22	syl5req 2488	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( X u. U. U. S ) = U. ( { X } u. U. S ) )
24		simpr 461	. . . . . . . . . . 11 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> S C_ (TopOn ` X ) )
25		toponuni 18554	. . . . . . . . . . . . . . 15 |- ( k e. (TopOn ` X ) -> X = U. k )
26		eqimss2 3430	. . . . . . . . . . . . . . 15 |- ( X = U. k -> U. k C_ X )
27	25, 26	syl 16	. . . . . . . . . . . . . 14 |- ( k e. (TopOn ` X ) -> U. k C_ X )
28		sspwuni 4277	. . . . . . . . . . . . . 14 |- ( k C_ ~P X <-> U. k C_ X )
29	27, 28	sylibr 212	. . . . . . . . . . . . 13 |- ( k e. (TopOn ` X ) -> k C_ ~P X )
30		selpw 3888	. . . . . . . . . . . . 13 |- ( k e. ~P ~P X <-> k C_ ~P X )
31	29, 30	sylibr 212	. . . . . . . . . . . 12 |- ( k e. (TopOn ` X ) -> k e. ~P ~P X )
32	31	ssriv 3381	. . . . . . . . . . 11 |- (TopOn ` X ) C_ ~P ~P X
33	24, 32	syl6ss 3389	. . . . . . . . . 10 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> S C_ ~P ~P X )
34		sspwuni 4277	. . . . . . . . . 10 |- ( S C_ ~P ~P X <-> U. S C_ ~P X )
35	33, 34	sylib 196	. . . . . . . . 9 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. S C_ ~P X )
36		sspwuni 4277	. . . . . . . . 9 |- ( U. S C_ ~P X <-> U. U. S C_ X )
37	35, 36	sylib 196	. . . . . . . 8 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. U. S C_ X )
38		ssequn2 3550	. . . . . . . 8 |- ( U. U. S C_ X <-> ( X u. U. U. S ) = X )
39	37, 38	sylib 196	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( X u. U. U. S ) = X )
40		snex 4554	. . . . . . . . 9 |- { X } e. _V
41		fvex 5722	. . . . . . . . . . . 12 |- (TopOn ` X ) e. _V
42	41	ssex 4457	. . . . . . . . . . 11 |- ( S C_ (TopOn ` X ) -> S e. _V )
43	42	adantl 466	. . . . . . . . . 10 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> S e. _V )
44		uniexg 6398	. . . . . . . . . 10 |- ( S e. _V -> U. S e. _V )
45	43, 44	syl 16	. . . . . . . . 9 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. S e. _V )
46		unexg 6402	. . . . . . . . 9 |- ( ( { X } e. _V /\ U. S e. _V ) -> ( { X } u. U. S ) e. _V )
47	40, 45, 46	sylancr 663	. . . . . . . 8 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( { X } u. U. S ) e. _V )
48		fiuni 7699	. . . . . . . 8 |- ( ( { X } u. U. S ) e. _V -> U. ( { X } u. U. S ) = U. ( fi ` ( { X } u. U. S ) ) )
49	47, 48	syl 16	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. ( { X } u. U. S ) = U. ( fi ` ( { X } u. U. S ) ) )
50	23, 39, 49	3eqtr3d 2483	. . . . . 6 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> X = U. ( fi ` ( { X } u. U. S ) ) )
51	50	fveq2d 5716	. . . . 5 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> (TopOn ` X ) = (TopOn ` U. ( fi ` ( { X } u. U. S ) ) ) )
52	18, 51	syl5eleqr 2530	. . . 4 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. (TopOn ` X ) )
53		elssuni 4142	. . . . . . . 8 |- ( j e. S -> j C_ U. S )
54		ssun2 3541	. . . . . . . 8 |- U. S C_ ( { X } u. U. S )
55	53, 54	syl6ss 3389	. . . . . . 7 |- ( j e. S -> j C_ ( { X } u. U. S ) )
56		ssfii 7690	. . . . . . . 8 |- ( ( { X } u. U. S ) e. _V -> ( { X } u. U. S ) C_ ( fi ` ( { X } u. U. S ) ) )
57	47, 56	syl 16	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( { X } u. U. S ) C_ ( fi ` ( { X } u. U. S ) ) )
58	55, 57	sylan9ssr 3391	. . . . . 6 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ j e. S ) -> j C_ ( fi ` ( { X } u. U. S ) ) )
59		bastg 18593	. . . . . . 7 |- ( ( fi ` ( { X } u. U. S ) ) e. TopBases -> ( fi ` ( { X } u. U. S ) ) C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) )
60	16, 59	ax-mp 5	. . . . . 6 |- ( fi ` ( { X } u. U. S ) ) C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) )
61	58, 60	syl6ss 3389	. . . . 5 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ j e. S ) -> j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) )
62	61	ralrimiva 2820	. . . 4 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> A. j e. S j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) )
63		sseq2 3399	. . . . . 6 |- ( k = ( topGen ` ( fi ` ( { X } u. U. S ) ) ) -> ( j C_ k <-> j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) ) )
64	63	ralbidv 2756	. . . . 5 |- ( k = ( topGen ` ( fi ` ( { X } u. U. S ) ) ) -> ( A. j e. S j C_ k <-> A. j e. S j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) ) )
65	64	elrab 3138	. . . 4 |- ( ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. { k e. (TopOn ` X ) | A. j e. S j C_ k } <-> ( ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. (TopOn ` X ) /\ A. j e. S j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) ) )
66	52, 62, 65	sylanbrc 664	. . 3 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. { k e. (TopOn ` X ) | A. j e. S j C_ k } )
67		intss1 4164	. . 3 |- ( ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. { k e. (TopOn ` X ) | A. j e. S j C_ k } -> |^| { k e. (TopOn ` X ) | A. j e. S j C_ k } C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) )
68	66, 67	syl 16	. 2 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> |^| { k e. (TopOn ` X ) | A. j e. S j C_ k } C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) )
69	15, 68	eqssd 3394	1 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) = |^| { k e. (TopOn ` X ) | A. j e. S j C_ k } )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2736   {crab 2740   _Vcvv 2993   u. cun 3347   C_ wss 3349   ~Pcpw 3881   {csn 3898   U.cuni 4112   |^|cint 4149   ` cfv 5439   ficfi 7681   topGenctg 14397   Topctop 18520  TopOnctopon 18521   TopBasesctb 18524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-recs 6853  df-rdg 6887  df-1o 6941  df-oadd 6945  df-er 7122  df-en 7332  df-fin 7335  df-fi 7682  df-topgen 14403  df-top 18525  df-bases 18527  df-topon 18528

This theorem is referenced by: (None)