Theorem 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	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		2onn	⊢ 2o ∈ ω
2		nnfi	⊢ ( 2o ∈ ω → 2o ∈ Fin )
3	1 2	ax-mp	⊢ 2o ∈ Fin
4		enfi	⊢ ( 𝑃 ≈ 2o → ( 𝑃 ∈ Fin ↔ 2o ∈ Fin ) )
5	3 4	mpbiri	⊢ ( 𝑃 ≈ 2o → 𝑃 ∈ Fin )
6	5	adantl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑃 ∈ Fin )
7		diffi	⊢ ( 𝑃 ∈ Fin → ( 𝑃 ∖ { 𝑋 } ) ∈ Fin )
8	6 7	syl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ∈ Fin )
9	8	cardidd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) ≈ ( 𝑃 ∖ { 𝑋 } ) )
10	9	ensymd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ≈ ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) )
11		simpl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑋 ∈ 𝑃 )
12		dif1card	⊢ ( ( 𝑃 ∈ Fin ∧ 𝑋 ∈ 𝑃 ) → ( card ‘ 𝑃 ) = suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) )
13	6 11 12	syl2anc	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ 𝑃 ) = suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) )
14		cardennn	⊢ ( ( 𝑃 ≈ 2o ∧ 2o ∈ ω ) → ( card ‘ 𝑃 ) = 2o )
15	1 14	mpan2	⊢ ( 𝑃 ≈ 2o → ( card ‘ 𝑃 ) = 2o )
16		df-2o	⊢ 2o = suc 1o
17	15 16	eqtrdi	⊢ ( 𝑃 ≈ 2o → ( card ‘ 𝑃 ) = suc 1o )
18	17	adantl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ 𝑃 ) = suc 1o )
19	13 18	eqtr3d	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = suc 1o )
20		cardon	⊢ ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) ∈ On
21		1on	⊢ 1o ∈ On
22		suc11	⊢ ( ( ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) ∈ On ∧ 1o ∈ On ) → ( suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = suc 1o ↔ ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = 1o ) )
23	20 21 22	mp2an	⊢ ( suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = suc 1o ↔ ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = 1o )
24	19 23	sylib	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = 1o )
25	10 24	breqtrd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ≈ 1o )
26		en1	⊢ ( ( 𝑃 ∖ { 𝑋 } ) ≈ 1o ↔ ∃ 𝑥 ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
27	25 26	sylib	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∃ 𝑥 ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
28		simplll	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → 𝑋 ∈ 𝑃 )
29	28	elexd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → 𝑋 ∈ V )
30		simplr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
31		sneqbg	⊢ ( 𝑋 ∈ 𝑃 → ( { 𝑋 } = { 𝑥 } ↔ 𝑋 = 𝑥 ) )
32	31	biimpar	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑋 = 𝑥 ) → { 𝑋 } = { 𝑥 } )
33	32	ad4ant14	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → { 𝑋 } = { 𝑥 } )
34	30 33	eqtr4d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑋 } )
35	34	ineq2d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( { 𝑋 } ∩ ( 𝑃 ∖ { 𝑋 } ) ) = ( { 𝑋 } ∩ { 𝑋 } ) )
36		disjdif	⊢ ( { 𝑋 } ∩ ( 𝑃 ∖ { 𝑋 } ) ) = ∅
37		inidm	⊢ ( { 𝑋 } ∩ { 𝑋 } ) = { 𝑋 }
38	35 36 37	3eqtr3g	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ∅ = { 𝑋 } )
39	38	eqcomd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → { 𝑋 } = ∅ )
40		snprc	⊢ ( ¬ 𝑋 ∈ V ↔ { 𝑋 } = ∅ )
41	39 40	sylibr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ¬ 𝑋 ∈ V )
42	29 41	pm2.65da	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ¬ 𝑋 = 𝑥 )
43	42	neqned	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑋 ≠ 𝑥 )
44		simpr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
45	44	unieqd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = ∪ { 𝑥 } )
46		unisnv	⊢ ∪ { 𝑥 } = 𝑥
47	45 46	eqtrdi	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = 𝑥 )
48	43 47	neeqtrrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑋 ≠ ∪ ( 𝑃 ∖ { 𝑋 } ) )
49	48	necomd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )
50	27 49	exlimddv	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )