Theorem topjoin 31014

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 19934	. . . . . . 7 |- ( k e. (TopOn ` X ) -> k e. Top )
2	1	ad2antrl 733	. . . . . 6 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> k e. Top )
3		toponmax 19936	. . . . . . . . 9 |- ( k e. (TopOn ` X ) -> X e. k )
4	3	ad2antrl 733	. . . . . . . 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 4116	. . . . . . 7 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ ( k e. (TopOn ` X ) /\ A. j e. S j C_ k ) ) -> { X } C_ k )
6		simprr 765	. . . . . . . 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 4228	. . . . . . . 8 |- ( U. S C_ k <-> A. j e. S j C_ k )
8	6, 7	sylibr 216	. . . . . . 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 3609	. . . . . 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 20000	. . . . . 6 |- ( ( k e. Top /\ ( { X } u. U. S ) C_ k ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) C_ k )
11	2, 9, 10	syl2anc 666	. . . . 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 619	. . . 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 2801	. . 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 4257	. . 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 216	. 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 19986	. . . . . 6 |- ( fi ` ( { X } u. U. S ) ) e. TopBases
17		tgtopon 19980	. . . . . 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 4216	. . . . . . . 8 |- U. ( { X } u. U. S ) = ( U. { X } u. U. U. S )
20		unisng 4213	. . . . . . . . . 10 |- ( X e. V -> U. { X } = X )
21	20	adantr 467	. . . . . . . . 9 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. { X } = X )
22	21	uneq1d 3586	. . . . . . . 8 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( U. { X } u. U. U. S ) = ( X u. U. U. S ) )
23	19, 22	syl5req 2497	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( X u. U. U. S ) = U. ( { X } u. U. S ) )
24		simpr 463	. . . . . . . . . . 11 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> S C_ (TopOn ` X ) )
25		toponuni 19935	. . . . . . . . . . . . . . 15 |- ( k e. (TopOn ` X ) -> X = U. k )
26		eqimss2 3484	. . . . . . . . . . . . . . 15 |- ( X = U. k -> U. k C_ X )
27	25, 26	syl 17	. . . . . . . . . . . . . 14 |- ( k e. (TopOn ` X ) -> U. k C_ X )
28		sspwuni 4366	. . . . . . . . . . . . . 14 |- ( k C_ ~P X <-> U. k C_ X )
29	27, 28	sylibr 216	. . . . . . . . . . . . 13 |- ( k e. (TopOn ` X ) -> k C_ ~P X )
30		selpw 3957	. . . . . . . . . . . . 13 |- ( k e. ~P ~P X <-> k C_ ~P X )
31	29, 30	sylibr 216	. . . . . . . . . . . 12 |- ( k e. (TopOn ` X ) -> k e. ~P ~P X )
32	31	ssriv 3435	. . . . . . . . . . 11 |- (TopOn ` X ) C_ ~P ~P X
33	24, 32	syl6ss 3443	. . . . . . . . . 10 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> S C_ ~P ~P X )
34		sspwuni 4366	. . . . . . . . . 10 |- ( S C_ ~P ~P X <-> U. S C_ ~P X )
35	33, 34	sylib 200	. . . . . . . . 9 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. S C_ ~P X )
36		sspwuni 4366	. . . . . . . . 9 |- ( U. S C_ ~P X <-> U. U. S C_ X )
37	35, 36	sylib 200	. . . . . . . 8 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. U. S C_ X )
38		ssequn2 3606	. . . . . . . 8 |- ( U. U. S C_ X <-> ( X u. U. U. S ) = X )
39	37, 38	sylib 200	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( X u. U. U. S ) = X )
40		snex 4640	. . . . . . . . 9 |- { X } e. _V
41		fvex 5873	. . . . . . . . . . . 12 |- (TopOn ` X ) e. _V
42	41	ssex 4546	. . . . . . . . . . 11 |- ( S C_ (TopOn ` X ) -> S e. _V )
43	42	adantl 468	. . . . . . . . . 10 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> S e. _V )
44		uniexg 6585	. . . . . . . . . 10 |- ( S e. _V -> U. S e. _V )
45	43, 44	syl 17	. . . . . . . . 9 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. S e. _V )
46		unexg 6589	. . . . . . . . 9 |- ( ( { X } e. _V /\ U. S e. _V ) -> ( { X } u. U. S ) e. _V )
47	40, 45, 46	sylancr 668	. . . . . . . 8 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( { X } u. U. S ) e. _V )
48		fiuni 7939	. . . . . . . 8 |- ( ( { X } u. U. S ) e. _V -> U. ( { X } u. U. S ) = U. ( fi ` ( { X } u. U. S ) ) )
49	47, 48	syl 17	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> U. ( { X } u. U. S ) = U. ( fi ` ( { X } u. U. S ) ) )
50	23, 39, 49	3eqtr3d 2492	. . . . . 6 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> X = U. ( fi ` ( { X } u. U. S ) ) )
51	50	fveq2d 5867	. . . . 5 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> (TopOn ` X ) = (TopOn ` U. ( fi ` ( { X } u. U. S ) ) ) )
52	18, 51	syl5eleqr 2535	. . . 4 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) e. (TopOn ` X ) )
53		elssuni 4226	. . . . . . . 8 |- ( j e. S -> j C_ U. S )
54		ssun2 3597	. . . . . . . 8 |- U. S C_ ( { X } u. U. S )
55	53, 54	syl6ss 3443	. . . . . . 7 |- ( j e. S -> j C_ ( { X } u. U. S ) )
56		ssfii 7930	. . . . . . . 8 |- ( ( { X } u. U. S ) e. _V -> ( { X } u. U. S ) C_ ( fi ` ( { X } u. U. S ) ) )
57	47, 56	syl 17	. . . . . . 7 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( { X } u. U. S ) C_ ( fi ` ( { X } u. U. S ) ) )
58	55, 57	sylan9ssr 3445	. . . . . 6 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ j e. S ) -> j C_ ( fi ` ( { X } u. U. S ) ) )
59		bastg 19974	. . . . . . 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 3443	. . . . 5 |- ( ( ( X e. V /\ S C_ (TopOn ` X ) ) /\ j e. S ) -> j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) )
62	61	ralrimiva 2801	. . . 4 |- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> A. j e. S j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) )
63		sseq2 3453	. . . . . 6 |- ( k = ( topGen ` ( fi ` ( { X } u. U. S ) ) ) -> ( j C_ k <-> j C_ ( topGen ` ( fi ` ( { X } u. U. S ) ) ) ) )
64	63	ralbidv 2826	. . . . 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 3195	. . . 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 669	. . 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 4248	. . 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 17	. 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 3448	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 371   = wceq 1443   e. wcel 1886   A.wral 2736   {crab 2740   _Vcvv 3044   u. cun 3401   C_ wss 3403   ~Pcpw 3950   {csn 3967   U.cuni 4197   |^|cint 4233   ` cfv 5581   ficfi 7921   topGenctg 15329   Topctop 19910  TopOnctopon 19911   TopBasesctb 19913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-oadd 7183  df-er 7360  df-en 7567  df-fin 7570  df-fi 7922  df-topgen 15335  df-top 19914  df-bases 19915  df-topon 19916

This theorem is referenced by: (None)