unidifsnel

Description: The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

		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		cardon	$⊢ card (P ∖ \{X\}) \in On$
21		1on	$⊢ 1_{𝑜} \in On$
22		suc11	$⊢ (card (P ∖ \{X\}) \in On \land 1_{𝑜} \in On) \to (suc card (P ∖ \{X\}) = suc 1_{𝑜} \leftrightarrow card (P ∖ \{X\}) = 1_{𝑜})$
23	20 21 22	mp2an	$⊢ suc card (P ∖ \{X\}) = suc 1_{𝑜} \leftrightarrow card (P ∖ \{X\}) = 1_{𝑜}$
24	19 23	sylib	$⊢ (X \in P \land P \approx 2_{𝑜}) \to card (P ∖ \{X\}) = 1_{𝑜}$
25	10 24	breqtrd	$⊢ (X \in P \land P \approx 2_{𝑜}) \to (P ∖ \{X\}) \approx 1_{𝑜}$
26		en1	$⊢ (P ∖ \{X\}) \approx 1_{𝑜} \leftrightarrow \exists x P ∖ \{X\} = \{x\}$
27	25 26	sylib	$⊢ (X \in P \land P \approx 2_{𝑜}) \to \exists x P ∖ \{X\} = \{x\}$
28		simpr	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to P ∖ \{X\} = \{x\}$
29	28	unieqd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) = ⋃ \{x\}$
30		unisnv	$⊢ ⋃ \{x\} = x$
31	29 30	eqtrdi	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) = x$
32		difssd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to P ∖ \{X\} \subseteq P$
33	28 32	eqsstrrd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to \{x\} \subseteq P$
34		vsnid	$⊢ x \in \{x\}$
35		ssel2	$⊢ (\{x\} \subseteq P \land x \in \{x\}) \to x \in P$
36	33 34 35	sylancl	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to x \in P$
37	31 36	eqeltrd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) \in P$
38	27 37	exlimddv	$⊢ (X \in P \land P \approx 2_{𝑜}) \to ⋃ (P ∖ \{X\}) \in P$

Metamath Proof Explorer

Theorem unidifsnel

Proof