Theorem 2oconcl

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

	Ref	Expression
Assertion	2oconcl	$$⊢A\in 2_{𝑜}\to 1_{𝑜}\setminus A\in 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		elpri	$$⊢A\in \left\{\varnothing ,1_{𝑜}\right\}\to \left(A=\varnothing \vee A=1_{𝑜}\right)$$
2		difeq2	$$⊢A=\varnothing \to 1_{𝑜}\setminus A=1_{𝑜}\setminus \varnothing$$
3		dif0	$$⊢1_{𝑜}\setminus \varnothing =1_{𝑜}$$
4	2 3	eqtrdi	$$⊢A=\varnothing \to 1_{𝑜}\setminus A=1_{𝑜}$$
5		difeq2	$$⊢A=1_{𝑜}\to 1_{𝑜}\setminus A=1_{𝑜}\setminus 1_{𝑜}$$
6		difid	$$⊢1_{𝑜}\setminus 1_{𝑜}=\varnothing$$
7	5 6	eqtrdi	$$⊢A=1_{𝑜}\to 1_{𝑜}\setminus A=\varnothing$$
8	4 7	orim12i	$$⊢\left(A=\varnothing \vee A=1_{𝑜}\right)\to \left(1_{𝑜}\setminus A=1_{𝑜}\vee 1_{𝑜}\setminus A=\varnothing \right)$$
9	8	orcomd	$$⊢\left(A=\varnothing \vee A=1_{𝑜}\right)\to \left(1_{𝑜}\setminus A=\varnothing \vee 1_{𝑜}\setminus A=1_{𝑜}\right)$$
10	1 9	syl	$$⊢A\in \left\{\varnothing ,1_{𝑜}\right\}\to \left(1_{𝑜}\setminus A=\varnothing \vee 1_{𝑜}\setminus A=1_{𝑜}\right)$$
11		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
12		difexg	$$⊢1_{𝑜}\in \mathrm{On}\to 1_{𝑜}\setminus A\in \mathrm{V}$$
13	11 12	ax-mp	$$⊢1_{𝑜}\setminus A\in \mathrm{V}$$
14	13	elpr	$$⊢1_{𝑜}\setminus A\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(1_{𝑜}\setminus A=\varnothing \vee 1_{𝑜}\setminus A=1_{𝑜}\right)$$
15	10 14	sylibr	$$⊢A\in \left\{\varnothing ,1_{𝑜}\right\}\to 1_{𝑜}\setminus A\in \left\{\varnothing ,1_{𝑜}\right\}$$
16		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
17	15 16	eleqtrrdi	$$⊢A\in \left\{\varnothing ,1_{𝑜}\right\}\to 1_{𝑜}\setminus A\in 2_{𝑜}$$
18	17 16	eleq2s	$$⊢A\in 2_{𝑜}\to 1_{𝑜}\setminus A\in 2_{𝑜}$$