Theorem ntruni

Description: A union of interiors is a subset of the interior of the union. The reverse inclusion may not hold. (Contributed by Jeff Hankins, 31-Aug-2009)

	Ref	Expression
Hypothesis	ntruni.1	|- X = U. J
Assertion	ntruni	|- ( ( J e. Top /\ O C_ ~P X ) -> U_ o e. O ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) )

Proof

Step	Hyp	Ref	Expression
1		ntruni.1	|- X = U. J
2		elssuni	|- ( o e. O -> o C_ U. O )
3		sspwuni	|- ( O C_ ~P X <-> U. O C_ X )
4	1	ntrss	|- ( ( J e. Top /\ U. O C_ X /\ o C_ U. O ) -> ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) )
5	4	3expia	|- ( ( J e. Top /\ U. O C_ X ) -> ( o C_ U. O -> ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) ) )
6	3 5	sylan2b	|- ( ( J e. Top /\ O C_ ~P X ) -> ( o C_ U. O -> ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) ) )
7	2 6	syl5	|- ( ( J e. Top /\ O C_ ~P X ) -> ( o e. O -> ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) ) )
8	7	ralrimiv	|- ( ( J e. Top /\ O C_ ~P X ) -> A. o e. O ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) )
9		iunss	|- ( U_ o e. O ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) <-> A. o e. O ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) )
10	8 9	sylibr	|- ( ( J e. Top /\ O C_ ~P X ) -> U_ o e. O ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) )