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

Metamath Proof Explorer

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 )