This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssunpr

Description: Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016)

		Ref	Expression
	Assertion	ssunpr	\|- ( ( B C_ A /\ A C_ ( B u. { C , D } ) ) <-> ( ( A = B \/ A = ( B u. { C } ) ) \/ ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-pr	\|- { C , D } = ( { C } u. { D } )
2	1	uneq2i	\|- ( B u. { C , D } ) = ( B u. ( { C } u. { D } ) )
3		unass	\|- ( ( B u. { C } ) u. { D } ) = ( B u. ( { C } u. { D } ) )
4	2 3	eqtr4i	\|- ( B u. { C , D } ) = ( ( B u. { C } ) u. { D } )
5	4	sseq2i	\|- ( A C_ ( B u. { C , D } ) <-> A C_ ( ( B u. { C } ) u. { D } ) )
6	5	anbi2i	\|- ( ( B C_ A /\ A C_ ( B u. { C , D } ) ) <-> ( B C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) )
7		ssunsn2	\|- ( ( B C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) <-> ( ( B C_ A /\ A C_ ( B u. { C } ) ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) ) )
8		ssunsn	\|- ( ( B C_ A /\ A C_ ( B u. { C } ) ) <-> ( A = B \/ A = ( B u. { C } ) ) )
9		un23	\|- ( ( B u. { C } ) u. { D } ) = ( ( B u. { D } ) u. { C } )
10	9	sseq2i	\|- ( A C_ ( ( B u. { C } ) u. { D } ) <-> A C_ ( ( B u. { D } ) u. { C } ) )
11	10	anbi2i	\|- ( ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) <-> ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { D } ) u. { C } ) ) )
12		ssunsn	\|- ( ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { D } ) u. { C } ) ) <-> ( A = ( B u. { D } ) \/ A = ( ( B u. { D } ) u. { C } ) ) )
13	4 9	eqtr2i	\|- ( ( B u. { D } ) u. { C } ) = ( B u. { C , D } )
14	13	eqeq2i	\|- ( A = ( ( B u. { D } ) u. { C } ) <-> A = ( B u. { C , D } ) )
15	14	orbi2i	\|- ( ( A = ( B u. { D } ) \/ A = ( ( B u. { D } ) u. { C } ) ) <-> ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) )
16	11 12 15	3bitri	\|- ( ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) <-> ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) )
17	8 16	orbi12i	\|- ( ( ( B C_ A /\ A C_ ( B u. { C } ) ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) ) <-> ( ( A = B \/ A = ( B u. { C } ) ) \/ ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) ) )
18	6 7 17	3bitri	\|- ( ( B C_ A /\ A C_ ( B u. { C , D } ) ) <-> ( ( A = B \/ A = ( B u. { C } ) ) \/ ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) ) )