en2eleq

Description: Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015)

		Ref	Expression
	Assertion	en2eleq	$⊢ (X \in P \land P \approx 2_{𝑜}) \to P = \{X, ⋃ (P ∖ \{X\})\}$

Proof

Step	Hyp	Ref	Expression
1		2onn	$⊢ 2_{𝑜} \in ω$
2		nnfi	$⊢ 2_{𝑜} \in ω \to 2_{𝑜} \in Fin$
3	1 2	ax-mp	$⊢ 2_{𝑜} \in Fin$
4		enfi	$⊢ P \approx 2_{𝑜} \to (P \in Fin \leftrightarrow 2_{𝑜} \in Fin)$
5	3 4	mpbiri	$⊢ P \approx 2_{𝑜} \to P \in Fin$
6	5	adantl	$⊢ (X \in P \land P \approx 2_{𝑜}) \to P \in Fin$
7		simpl	$⊢ (X \in P \land P \approx 2_{𝑜}) \to X \in P$
8		1onn	$⊢ 1_{𝑜} \in ω$
9		simpr	$⊢ (X \in P \land P \approx 2_{𝑜}) \to P \approx 2_{𝑜}$
10		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
11	9 10	breqtrdi	$⊢ (X \in P \land P \approx 2_{𝑜}) \to P \approx suc 1_{𝑜}$
12		dif1ennn	$⊢ (1_{𝑜} \in ω \land P \approx suc 1_{𝑜} \land X \in P) \to (P ∖ \{X\}) \approx 1_{𝑜}$
13	8 11 7 12	mp3an2i	$⊢ (X \in P \land P \approx 2_{𝑜}) \to (P ∖ \{X\}) \approx 1_{𝑜}$
14		en1uniel	$⊢ (P ∖ \{X\}) \approx 1_{𝑜} \to ⋃ (P ∖ \{X\}) \in (P ∖ \{X\})$
15	13 14	syl	$⊢ (X \in P \land P \approx 2_{𝑜}) \to ⋃ (P ∖ \{X\}) \in (P ∖ \{X\})$
16		eldifsn	$⊢ ⋃ (P ∖ \{X\}) \in (P ∖ \{X\}) \leftrightarrow (⋃ (P ∖ \{X\}) \in P \land ⋃ (P ∖ \{X\}) \neq X)$
17	15 16	sylib	$⊢ (X \in P \land P \approx 2_{𝑜}) \to (⋃ (P ∖ \{X\}) \in P \land ⋃ (P ∖ \{X\}) \neq X)$
18	17	simpld	$⊢ (X \in P \land P \approx 2_{𝑜}) \to ⋃ (P ∖ \{X\}) \in P$
19	7 18	prssd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to \{X, ⋃ (P ∖ \{X\})\} \subseteq P$
20	17	simprd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to ⋃ (P ∖ \{X\}) \neq X$
21	20	necomd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to X \neq ⋃ (P ∖ \{X\})$
22		enpr2	$⊢ (X \in P \land ⋃ (P ∖ \{X\}) \in P \land X \neq ⋃ (P ∖ \{X\})) \to \{X, ⋃ (P ∖ \{X\})\} \approx 2_{𝑜}$
23	7 18 21 22	syl3anc	$⊢ (X \in P \land P \approx 2_{𝑜}) \to \{X, ⋃ (P ∖ \{X\})\} \approx 2_{𝑜}$
24		ensym	$⊢ P \approx 2_{𝑜} \to 2_{𝑜} \approx P$
25	24	adantl	$⊢ (X \in P \land P \approx 2_{𝑜}) \to 2_{𝑜} \approx P$
26		entr	$⊢ (\{X, ⋃ (P ∖ \{X\})\} \approx 2_{𝑜} \land 2_{𝑜} \approx P) \to \{X, ⋃ (P ∖ \{X\})\} \approx P$
27	23 25 26	syl2anc	$⊢ (X \in P \land P \approx 2_{𝑜}) \to \{X, ⋃ (P ∖ \{X\})\} \approx P$
28		fisseneq	$⊢ (P \in Fin \land \{X, ⋃ (P ∖ \{X\})\} \subseteq P \land \{X, ⋃ (P ∖ \{X\})\} \approx P) \to \{X, ⋃ (P ∖ \{X\})\} = P$
29	6 19 27 28	syl3anc	$⊢ (X \in P \land P \approx 2_{𝑜}) \to \{X, ⋃ (P ∖ \{X\})\} = P$
30	29	eqcomd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to P = \{X, ⋃ (P ∖ \{X\})\}$

Metamath Proof Explorer

Theorem en2eleq

Proof