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_{𝑜} ∖ A \in 2_{𝑜}$

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

Metamath Proof Explorer