unidifsnel

Description: The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017)

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

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		diffi	$⊢ P \in Fin \to P ∖ \{X\} \in Fin$
8	6 7	syl	$⊢ (X \in P \land P \approx 2_{𝑜}) \to P ∖ \{X\} \in Fin$
9	8	cardidd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to card (P ∖ \{X\}) \approx (P ∖ \{X\})$
10	9	ensymd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to (P ∖ \{X\}) \approx card (P ∖ \{X\})$
11		simpl	$⊢ (X \in P \land P \approx 2_{𝑜}) \to X \in P$
12		dif1card	$⊢ (P \in Fin \land X \in P) \to card (P) = suc card (P ∖ \{X\})$
13	6 11 12	syl2anc	$⊢ (X \in P \land P \approx 2_{𝑜}) \to card (P) = suc card (P ∖ \{X\})$
14		cardennn	$⊢ (P \approx 2_{𝑜} \land 2_{𝑜} \in ω) \to card (P) = 2_{𝑜}$
15	1 14	mpan2	$⊢ P \approx 2_{𝑜} \to card (P) = 2_{𝑜}$
16		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
17	15 16	eqtrdi	$⊢ P \approx 2_{𝑜} \to card (P) = suc 1_{𝑜}$
18	17	adantl	$⊢ (X \in P \land P \approx 2_{𝑜}) \to card (P) = suc 1_{𝑜}$
19	13 18	eqtr3d	$⊢ (X \in P \land P \approx 2_{𝑜}) \to suc card (P ∖ \{X\}) = suc 1_{𝑜}$
20		suc11reg	$⊢ suc card (P ∖ \{X\}) = suc 1_{𝑜} \leftrightarrow card (P ∖ \{X\}) = 1_{𝑜}$
21	19 20	sylib	$⊢ (X \in P \land P \approx 2_{𝑜}) \to card (P ∖ \{X\}) = 1_{𝑜}$
22	10 21	breqtrd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to (P ∖ \{X\}) \approx 1_{𝑜}$
23		en1	$⊢ (P ∖ \{X\}) \approx 1_{𝑜} \leftrightarrow \exists x P ∖ \{X\} = \{x\}$
24	22 23	sylib	$⊢ (X \in P \land P \approx 2_{𝑜}) \to \exists x P ∖ \{X\} = \{x\}$
25		simpr	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to P ∖ \{X\} = \{x\}$
26	25	unieqd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) = ⋃ \{x\}$
27		unisnv	$⊢ ⋃ \{x\} = x$
28	26 27	eqtrdi	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) = x$
29		difssd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to P ∖ \{X\} \subseteq P$
30	25 29	eqsstrrd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to \{x\} \subseteq P$
31		vsnid	$⊢ x \in \{x\}$
32		ssel2	$⊢ (\{x\} \subseteq P \land x \in \{x\}) \to x \in P$
33	30 31 32	sylancl	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to x \in P$
34	28 33	eqeltrd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) \in P$
35	24 34	exlimddv	$⊢ (X \in P \land P \approx 2_{𝑜}) \to ⋃ (P ∖ \{X\}) \in P$

Metamath Proof Explorer

Theorem unidifsnel

Proof