Theorem unidifsnne

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

	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		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		simplll	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → 𝑋 ∈ 𝑃 )
26	25	elexd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → 𝑋 ∈ V )
27		simplr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
28		sneqbg	⊢ ( 𝑋 ∈ 𝑃 → ( { 𝑋 } = { 𝑥 } ↔ 𝑋 = 𝑥 ) )
29	28	biimpar	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑋 = 𝑥 ) → { 𝑋 } = { 𝑥 } )
30	29	ad4ant14	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → { 𝑋 } = { 𝑥 } )
31	27 30	eqtr4d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑋 } )
32	31	ineq2d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ( { 𝑋 } ∩ ( 𝑃 ∖ { 𝑋 } ) ) = ( { 𝑋 } ∩ { 𝑋 } ) )
33		disjdif	⊢ ( { 𝑋 } ∩ ( 𝑃 ∖ { 𝑋 } ) ) = ∅
34		inidm	⊢ ( { 𝑋 } ∩ { 𝑋 } ) = { 𝑋 }
35	32 33 34	3eqtr3g	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ∅ = { 𝑋 } )
36	35	eqcomd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → { 𝑋 } = ∅ )
37		snprc	⊢ ( ¬ 𝑋 ∈ V ↔ { 𝑋 } = ∅ )
38	36 37	sylibr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) ∧ 𝑋 = 𝑥 ) → ¬ 𝑋 ∈ V )
39	26 38	pm2.65da	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ¬ 𝑋 = 𝑥 )
40	39	neqned	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑋 ≠ 𝑥 )
41		simpr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } )
42	41	unieqd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = ∪ { 𝑥 } )
43		vex	⊢ 𝑥 ∈ V
44	43	unisn	⊢ ∪ { 𝑥 } = 𝑥
45	42 44	eqtrdi	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) = 𝑥 )
46	40 45	neeqtrrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → 𝑋 ≠ ∪ ( 𝑃 ∖ { 𝑋 } ) )
47	46	necomd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) ∧ ( 𝑃 ∖ { 𝑋 } ) = { 𝑥 } ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )
48	24 47	exlimddv	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → ∪ ( 𝑃 ∖ { 𝑋 } ) ≠ 𝑋 )