Theorem unidifsnel

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

	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		suc11reg	⊢ ( suc ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = suc 1o ↔ ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = 1o )
21	19 20	sylib	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( card ‘ ( 𝑃 ∖ { 𝑋 } ) ) = 1o )
22	10 21	breqtrd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∖ { 𝑋 } ) ≈ 1o )
23		en1	⊢ ( ( 𝑃 ∖ { 𝑋 } ) ≈ 1o ↔ ∃ 𝑥 ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
24	22 23	sylib	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∃ 𝑥 ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
25		simpr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
26	25	unieqd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = ∪ { 𝑥 } )
27		vex	⊢ 𝑥 ∈ V
28	27	unisn	⊢ ∪ { 𝑥 } = 𝑥
29	26 28	eqtrdi	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = 𝑥 )
30		difssd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) ⊆ 𝑃 )
31	25 30	eqsstrrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → { 𝑥 } ⊆ 𝑃 )
32		vsnid	⊢ 𝑥 ∈ { 𝑥 }
33		ssel2	⊢ ( ( { 𝑥 } ⊆ 𝑃 ∧ 𝑥 ∈ { 𝑥 } ) → 𝑥 ∈ 𝑃 )
34	31 32 33	sylancl	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑥 ∈ 𝑃 )
35	29 34	eqeltrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ 𝑃 )
36	24 35	exlimddv	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ∈ 𝑃 )