Theorem 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	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 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		simpr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
29	28	unieqd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = ∪ { 𝑥 } )
30		unisnv	⊢ ∪ { 𝑥 } = 𝑥
31	29 30	eqtrdi	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = 𝑥 )
32		difssd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) ⊆ 𝑃 )
33	28 32	eqsstrrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → { 𝑥 } ⊆ 𝑃 )
34		vsnid	⊢ 𝑥 ∈ { 𝑥 }
35		ssel2	⊢ ( ( { 𝑥 } ⊆ 𝑃 ∧ 𝑥 ∈ { 𝑥 } ) → 𝑥 ∈ 𝑃 )
36	33 34 35	sylancl	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑥 ∈ 𝑃 )
37	31 36	eqeltrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ 𝑃 )
38	27 37	exlimddv	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ 𝑃 )