unidifsnne

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

		Ref	Expression
	Assertion	unidifsnne	$⊢ (X \in P \land P \approx 2_{𝑜}) \to ⋃ (P ∖ \{X\}) \neq 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		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		simplll	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to X \in P$
29	28	elexd	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to X \in V$
30		simplr	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to P ∖ \{X\} = \{x\}$
31		sneqbg	$⊢ X \in P \to (\{X\} = \{x\} \leftrightarrow X = x)$
32	31	biimpar	$⊢ (X \in P \land X = x) \to \{X\} = \{x\}$
33	32	ad4ant14	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to \{X\} = \{x\}$
34	30 33	eqtr4d	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to P ∖ \{X\} = \{X\}$
35	34	ineq2d	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to \{X\} \cap (P ∖ \{X\}) = \{X\} \cap \{X\}$
36		disjdif	$⊢ \{X\} \cap (P ∖ \{X\}) = \emptyset$
37		inidm	$⊢ \{X\} \cap \{X\} = \{X\}$
38	35 36 37	3eqtr3g	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to \emptyset = \{X\}$
39	38	eqcomd	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to \{X\} = \emptyset$
40		snprc	$⊢ \neg X \in V \leftrightarrow \{X\} = \emptyset$
41	39 40	sylibr	$⊢ (((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \land X = x) \to \neg X \in V$
42	29 41	pm2.65da	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to \neg X = x$
43	42	neqned	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to X \neq x$
44		simpr	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to P ∖ \{X\} = \{x\}$
45	44	unieqd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) = ⋃ \{x\}$
46		unisnv	$⊢ ⋃ \{x\} = x$
47	45 46	eqtrdi	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) = x$
48	43 47	neeqtrrd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to X \neq ⋃ (P ∖ \{X\})$
49	48	necomd	$⊢ ((X \in P \land P \approx 2_{𝑜}) \land P ∖ \{X\} = \{x\}) \to ⋃ (P ∖ \{X\}) \neq X$
50	27 49	exlimddv	$⊢ (X \in P \land P \approx 2_{𝑜}) \to ⋃ (P ∖ \{X\}) \neq X$

Metamath Proof Explorer

Theorem unidifsnne

Proof