Metamath Proof Explorer

Theorem iinopn

Description: The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Assertion iinopn 
|- ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> |^|_ x e. A B e. J )

Proof

Step Hyp Ref Expression
1 simpr3 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> A. x e. A B e. J )
2 dfiin2g 
 |-  ( A. x e. A B e. J -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
3 1 2 syl 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
4 simpl 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> J e. Top )
5 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
6 5 rnmpt 
 |-  ran ( x e. A |-> B ) = { y | E. x e. A y = B }
7 5 fmpt 
 |-  ( A. x e. A B e. J <-> ( x e. A |-> B ) : A --> J )
8 1 7 sylib 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> ( x e. A |-> B ) : A --> J )
9 8 frnd 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> ran ( x e. A |-> B ) C_ J )
10 6 9 eqsstrrid 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> { y | E. x e. A y = B } C_ J )
11 8 fdmd 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> dom ( x e. A |-> B ) = A )
12 simpr2 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> A =/= (/) )
13 11 12 eqnetrd 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> dom ( x e. A |-> B ) =/= (/) )
14 dm0rn0 
 |-  ( dom ( x e. A |-> B ) = (/) <-> ran ( x e. A |-> B ) = (/) )
15 6 eqeq1i 
 |-  ( ran ( x e. A |-> B ) = (/) <-> { y | E. x e. A y = B } = (/) )
16 14 15 bitri 
 |-  ( dom ( x e. A |-> B ) = (/) <-> { y | E. x e. A y = B } = (/) )
17 16 necon3bii 
 |-  ( dom ( x e. A |-> B ) =/= (/) <-> { y | E. x e. A y = B } =/= (/) )
18 13 17 sylib 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> { y | E. x e. A y = B } =/= (/) )
19 simpr1 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> A e. Fin )
20 abrexfi 
 |-  ( A e. Fin -> { y | E. x e. A y = B } e. Fin )
21 19 20 syl 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> { y | E. x e. A y = B } e. Fin )
22 fiinopn 
 |-  ( J e. Top -> ( ( { y | E. x e. A y = B } C_ J /\ { y | E. x e. A y = B } =/= (/) /\ { y | E. x e. A y = B } e. Fin ) -> |^| { y | E. x e. A y = B } e. J ) )
23 22 imp 
 |-  ( ( J e. Top /\ ( { y | E. x e. A y = B } C_ J /\ { y | E. x e. A y = B } =/= (/) /\ { y | E. x e. A y = B } e. Fin ) ) -> |^| { y | E. x e. A y = B } e. J )
24 4 10 18 21 23 syl13anc 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> |^| { y | E. x e. A y = B } e. J )
25 3 24 eqeltrd 
 |-  ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> |^|_ x e. A B e. J )