Theorem 2oconcl

Description: Closure of the pair swapping function on 2o . (Contributed by Mario Carneiro, 27-Sep-2015)

	Ref	Expression
Assertion	2oconcl	|- ( A e. 2o -> ( 1o \ A ) e. 2o )

Proof

Step	Hyp	Ref	Expression
1		elpri	|- ( A e. { (/) , 1o } -> ( A = (/) \/ A = 1o ) )
2		difeq2	|- ( A = (/) -> ( 1o \ A ) = ( 1o \ (/) ) )
3		dif0	|- ( 1o \ (/) ) = 1o
4	2 3	eqtrdi	|- ( A = (/) -> ( 1o \ A ) = 1o )
5		difeq2	|- ( A = 1o -> ( 1o \ A ) = ( 1o \ 1o ) )
6		difid	|- ( 1o \ 1o ) = (/)
7	5 6	eqtrdi	|- ( A = 1o -> ( 1o \ A ) = (/) )
8	4 7	orim12i	|- ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = 1o \/ ( 1o \ A ) = (/) ) )
9	8	orcomd	|- ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
10	1 9	syl	|- ( A e. { (/) , 1o } -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
11		1on	|- 1o e. On
12		difexg	|- ( 1o e. On -> ( 1o \ A ) e. _V )
13	11 12	ax-mp	|- ( 1o \ A ) e. _V
14	13	elpr	|- ( ( 1o \ A ) e. { (/) , 1o } <-> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
15	10 14	sylibr	|- ( A e. { (/) , 1o } -> ( 1o \ A ) e. { (/) , 1o } )
16		df2o3	|- 2o = { (/) , 1o }
17	15 16	eleqtrrdi	|- ( A e. { (/) , 1o } -> ( 1o \ A ) e. 2o )
18	17 16	eleq2s	|- ( A e. 2o -> ( 1o \ A ) e. 2o )