Metamath Proof Explorer


Theorem dju1dif

Description: Adding and subtracting one gives back the original cardinality. Similar to pncan for cardinalities. (Contributed by Mario Carneiro, 18-May-2015) (Revised by Jim Kingdon, 20-Aug-2023)

Ref Expression
Assertion dju1dif A V B A ⊔︀ 1 𝑜 A ⊔︀ 1 𝑜 B A

Proof

Step Hyp Ref Expression
1 simpl A V B A ⊔︀ 1 𝑜 A V
2 1oex 1 𝑜 V
3 djuex A V 1 𝑜 V A ⊔︀ 1 𝑜 V
4 1 2 3 sylancl A V B A ⊔︀ 1 𝑜 A ⊔︀ 1 𝑜 V
5 simpr A V B A ⊔︀ 1 𝑜 B A ⊔︀ 1 𝑜
6 df1o2 1 𝑜 =
7 6 xpeq2i 1 𝑜 × 1 𝑜 = 1 𝑜 ×
8 0ex V
9 2 8 xpsn 1 𝑜 × = 1 𝑜
10 7 9 eqtri 1 𝑜 × 1 𝑜 = 1 𝑜
11 ssun2 1 𝑜 × 1 𝑜 × A 1 𝑜 × 1 𝑜
12 10 11 eqsstrri 1 𝑜 × A 1 𝑜 × 1 𝑜
13 opex 1 𝑜 V
14 13 snss 1 𝑜 × A 1 𝑜 × 1 𝑜 1 𝑜 × A 1 𝑜 × 1 𝑜
15 12 14 mpbir 1 𝑜 × A 1 𝑜 × 1 𝑜
16 df-dju A ⊔︀ 1 𝑜 = × A 1 𝑜 × 1 𝑜
17 15 16 eleqtrri 1 𝑜 A ⊔︀ 1 𝑜
18 17 a1i A V B A ⊔︀ 1 𝑜 1 𝑜 A ⊔︀ 1 𝑜
19 difsnen A ⊔︀ 1 𝑜 V B A ⊔︀ 1 𝑜 1 𝑜 A ⊔︀ 1 𝑜 A ⊔︀ 1 𝑜 B A ⊔︀ 1 𝑜 1 𝑜
20 4 5 18 19 syl3anc A V B A ⊔︀ 1 𝑜 A ⊔︀ 1 𝑜 B A ⊔︀ 1 𝑜 1 𝑜
21 16 difeq1i A ⊔︀ 1 𝑜 1 𝑜 = × A 1 𝑜 × 1 𝑜 1 𝑜
22 xp01disjl × A 1 𝑜 × 1 𝑜 =
23 disj3 × A 1 𝑜 × 1 𝑜 = × A = × A 1 𝑜 × 1 𝑜
24 22 23 mpbi × A = × A 1 𝑜 × 1 𝑜
25 difun2 × A 1 𝑜 × 1 𝑜 1 𝑜 × 1 𝑜 = × A 1 𝑜 × 1 𝑜
26 10 difeq2i × A 1 𝑜 × 1 𝑜 1 𝑜 × 1 𝑜 = × A 1 𝑜 × 1 𝑜 1 𝑜
27 24 25 26 3eqtr2i × A = × A 1 𝑜 × 1 𝑜 1 𝑜
28 21 27 eqtr4i A ⊔︀ 1 𝑜 1 𝑜 = × A
29 xpsnen2g V A V × A A
30 8 1 29 sylancr A V B A ⊔︀ 1 𝑜 × A A
31 28 30 eqbrtrid A V B A ⊔︀ 1 𝑜 A ⊔︀ 1 𝑜 1 𝑜 A
32 entr A ⊔︀ 1 𝑜 B A ⊔︀ 1 𝑜 1 𝑜 A ⊔︀ 1 𝑜 1 𝑜 A A ⊔︀ 1 𝑜 B A
33 20 31 32 syl2anc A V B A ⊔︀ 1 𝑜 A ⊔︀ 1 𝑜 B A