Theorem 2oconcl 6150

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

Assertion

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

Proof of Theorem 2oconcl

Step	Hyp	Ref	Expression
1		elpri 3453	. . . . 5 |- ( A e. { (/) , 1o } -> ( A = (/) \/ A = 1o ) )
2		difeq2 3101	. . . . . . . 8 |- ( A = (/) -> ( 1o \ A ) = ( 1o \ (/) ) )
3		dif0 3341	. . . . . . . 8 |- ( 1o \ (/) ) = 1o
4	2, 3	syl6eq 2133	. . . . . . 7 |- ( A = (/) -> ( 1o \ A ) = 1o )
5		difeq2 3101	. . . . . . . 8 |- ( A = 1o -> ( 1o \ A ) = ( 1o \ 1o ) )
6		difid 3339	. . . . . . . 8 |- ( 1o \ 1o ) = (/)
7	5, 6	syl6eq 2133	. . . . . . 7 |- ( A = 1o -> ( 1o \ A ) = (/) )
8	4, 7	orim12i 709	. . . . . 6 |- ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = 1o \/ ( 1o \ A ) = (/) ) )
9	8	orcomd 681	. . . . 5 |- ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
10	1, 9	syl 14	. . . 4 |- ( A e. { (/) , 1o } -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
11		1on 6135	. . . . . 6 |- 1o e. On
12		difexg 3953	. . . . . 6 |- ( 1o e. On -> ( 1o \ A ) e. _V )
13	11, 12	ax-mp 7	. . . . 5 |- ( 1o \ A ) e. _V
14	13	elpr 3451	. . . 4 |- ( ( 1o \ A ) e. { (/) , 1o } <-> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) )
15	10, 14	sylibr 132	. . 3 |- ( A e. { (/) , 1o } -> ( 1o \ A ) e. { (/) , 1o } )
16		df2o3 6142	. . 3 |- 2o = { (/) , 1o }
17	15, 16	syl6eleqr 2178	. 2 |- ( A e. { (/) , 1o } -> ( 1o \ A ) e. 2o )
18	17, 16	eleq2s 2179	1 |- ( A e. 2o -> ( 1o \ A ) e. 2o )

Syntax hints:   -> wi 4   \/ wo 662   = wceq 1287   e. wcel 1436   _Vcvv 2615   \ cdif 2985   (/)c0 3275   {cpr 3431   Oncon0 4162   1oc1o 6121   2oc2o 6122

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3930  ax-nul 3938  ax-pow 3982  ax-pr 4008  ax-un 4232

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3416  df-sn 3436  df-pr 3437  df-uni 3636  df-tr 3910  df-iord 4165  df-on 4167  df-suc 4170  df-1o 6128  df-2o 6129

This theorem is referenced by: (None)