Metamath Proof Explorer

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 ⊢ X ∈ P ∧ P ≈ 2 𝑜 → ⋃ P ∖ X ∈ P

Proof

Step Hyp Ref Expression
1 2onn ⊢ 2 𝑜 ∈ ω
2 nnfi ⊢ 2 𝑜 ∈ ω → 2 𝑜 ∈ Fin
3 1 2 ax-mp ⊢ 2 𝑜 ∈ Fin
4 enfi ⊢ P ≈ 2 𝑜 → P ∈ Fin ↔ 2 𝑜 ∈ Fin
5 3 4 mpbiri ⊢ P ≈ 2 𝑜 → P ∈ Fin
6 5 adantl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ∈ Fin
7 diffi ⊢ P ∈ Fin → P ∖ X ∈ Fin
8 6 7 syl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ∖ X ∈ Fin
9 8 cardidd ⊢ X ∈ P ∧ P ≈ 2 𝑜 → card ⁡ P ∖ X ≈ P ∖ X
10 9 ensymd ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ∖ X ≈ card ⁡ P ∖ X
11 simpl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → X ∈ P
12 dif1card ⊢ P ∈ Fin ∧ X ∈ P → card ⁡ P = suc ⁡ card ⁡ P ∖ X
13 6 11 12 syl2anc ⊢ X ∈ P ∧ P ≈ 2 𝑜 → card ⁡ P = suc ⁡ card ⁡ P ∖ X
14 cardennn ⊢ P ≈ 2 𝑜 ∧ 2 𝑜 ∈ ω → card ⁡ P = 2 𝑜
15 1 14 mpan2 ⊢ P ≈ 2 𝑜 → card ⁡ P = 2 𝑜
16 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
17 15 16 eqtrdi ⊢ P ≈ 2 𝑜 → card ⁡ P = suc ⁡ 1 𝑜
18 17 adantl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → card ⁡ P = suc ⁡ 1 𝑜
19 13 18 eqtr3d ⊢ X ∈ P ∧ P ≈ 2 𝑜 → suc ⁡ card ⁡ P ∖ X = suc ⁡ 1 𝑜
20 suc11reg ⊢ suc ⁡ card ⁡ P ∖ X = suc ⁡ 1 𝑜 ↔ card ⁡ P ∖ X = 1 𝑜
21 19 20 sylib ⊢ X ∈ P ∧ P ≈ 2 𝑜 → card ⁡ P ∖ X = 1 𝑜
22 10 21 breqtrd ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ∖ X ≈ 1 𝑜
23 en1 ⊢ P ∖ X ≈ 1 𝑜 ↔ ∃ x P ∖ X = x
24 22 23 sylib ⊢ X ∈ P ∧ P ≈ 2 𝑜 → ∃ x P ∖ X = x
25 simpr ⊢ X ∈ P ∧ P ≈ 2 𝑜 ∧ P ∖ X = x → P ∖ X = x
26 25 unieqd ⊢ X ∈ P ∧ P ≈ 2 𝑜 ∧ P ∖ X = x → ⋃ P ∖ X = ⋃ x
27 unisnv ⊢ ⋃ x = x
28 26 27 eqtrdi ⊢ X ∈ P ∧ P ≈ 2 𝑜 ∧ P ∖ X = x → ⋃ P ∖ X = x
29 difssd ⊢ X ∈ P ∧ P ≈ 2 𝑜 ∧ P ∖ X = x → P ∖ X ⊆ P
30 25 29 eqsstrrd ⊢ X ∈ P ∧ P ≈ 2 𝑜 ∧ P ∖ X = x → x ⊆ P
31 vsnid ⊢ x ∈ x
32 ssel2 ⊢ x ⊆ P ∧ x ∈ x → x ∈ P
33 30 31 32 sylancl ⊢ X ∈ P ∧ P ≈ 2 𝑜 ∧ P ∖ X = x → x ∈ P
34 28 33 eqeltrd ⊢ X ∈ P ∧ P ≈ 2 𝑜 ∧ P ∖ X = x → ⋃ P ∖ X ∈ P
35 24 34 exlimddv ⊢ X ∈ P ∧ P ≈ 2 𝑜 → ⋃ P ∖ X ∈ P