Theorem inttop4 14865

Description: The intersection of two topologies is a topology.

Assertion

Ref	Expression
inttop4	|- ((J e. Top /\ K e. Top) -> (J i^i K) e. Top)

Proof of Theorem inttop4

Step	Hyp	Ref	Expression
1		prssg 3140	. . . 4 |- ((J e. Top /\ K e. Top) -> ((J e. Top /\ K e. Top) <-> {J, K} C_ Top))
2	1	biimpd 170	. . 3 |- ((J e. Top /\ K e. Top) -> ((J e. Top /\ K e. Top) -> {J, K} C_ Top))
3		intprg 3251	. . . . . . 7 |- ((J e. Top /\ K e. Top) -> |^|{J, K} = (J i^i K))
4	3	eqcomd 1889	. . . . . 6 |- ((J e. Top /\ K e. Top) -> (J i^i K) = |^|{J, K})
5	4	adantl 424	. . . . 5 |- (({J, K} C_ Top /\ (J e. Top /\ K e. Top)) -> (J i^i K) = |^|{J, K})
6		prnzg 14454	. . . . . . . 8 |- (J e. Top -> {J, K} =/= (/))
7		inttop3 14864	. . . . . . . . 9 |- (({J, K} =/= (/) /\ {J, K} C_ Top) -> |^|{J, K} e. Top)
8	7	ex 402	. . . . . . . 8 |- ({J, K} =/= (/) -> ({J, K} C_ Top -> |^|{J, K} e. Top))
9	6, 8	syl 12	. . . . . . 7 |- (J e. Top -> ({J, K} C_ Top -> |^|{J, K} e. Top))
10	9	adantr 425	. . . . . 6 |- ((J e. Top /\ K e. Top) -> ({J, K} C_ Top -> |^|{J, K} e. Top))
11	10	impcom 378	. . . . 5 |- (({J, K} C_ Top /\ (J e. Top /\ K e. Top)) -> |^|{J, K} e. Top)
12	5, 11	eqeltrd 1971	. . . 4 |- (({J, K} C_ Top /\ (J e. Top /\ K e. Top)) -> (J i^i K) e. Top)
13	12	ex 402	. . 3 |- ({J, K} C_ Top -> ((J e. Top /\ K e. Top) -> (J i^i K) e. Top))
14	2, 13	syli 65	. 2 |- ((J e. Top /\ K e. Top) -> ((J e. Top /\ K e. Top) -> (J i^i K) e. Top))
15	14	pm2.43i 78	1 |- ((J e. Top /\ K e. Top) -> (J i^i K) e. Top)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300   =/= wne 2017   i^i cin 2592   C_ wss 2593  (/)c0 2875  {cpr 3045  |^|cint 3214  Topctop 8857

This theorem is referenced by:  intcont 14914

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-sep 3438  ax-nul 3445  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-uni 3178  df-int 3215  df-iin 3258  df-top 8861

Copyright terms: Public domain