unidifsnne

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

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

Metamath Proof Explorer

Theorem unidifsnne

Proof