This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → ( ( 𝐴 ⊔ 1o ) ∖ { 𝐵 } ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → 𝐴 ∈ 𝑉 )
2 1oex ⊢ 1o ∈ V
3 djuex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1o ∈ V ) → ( 𝐴 ⊔ 1o ) ∈ V )
4 1 2 3 sylancl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → ( 𝐴 ⊔ 1o ) ∈ V )
5 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → 𝐵 ∈ ( 𝐴 ⊔ 1o ) )
6 df1o2 ⊢ 1o = { ∅ }
7 6 xpeq2i ⊢ ( { 1o } × 1o ) = ( { 1o } × { ∅ } )
8 0ex ⊢ ∅ ∈ V
9 2 8 xpsn ⊢ ( { 1o } × { ∅ } ) = { ⟨ 1o , ∅ ⟩ }
10 7 9 eqtri ⊢ ( { 1o } × 1o ) = { ⟨ 1o , ∅ ⟩ }
11 ssun2 ⊢ ( { 1o } × 1o ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
12 10 11 eqsstrri ⊢ { ⟨ 1o , ∅ ⟩ } ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
13 opex ⊢ ⟨ 1o , ∅ ⟩ ∈ V
14 13 snss ⊢ ( ⟨ 1o , ∅ ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ↔ { ⟨ 1o , ∅ ⟩ } ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) )
15 12 14 mpbir ⊢ ⟨ 1o , ∅ ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
16 df-dju ⊢ ( 𝐴 ⊔ 1o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
17 15 16 eleqtrri ⊢ ⟨ 1o , ∅ ⟩ ∈ ( 𝐴 ⊔ 1o )
18 17 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → ⟨ 1o , ∅ ⟩ ∈ ( 𝐴 ⊔ 1o ) )
19 difsnen ⊢ ( ( ( 𝐴 ⊔ 1o ) ∈ V ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ∧ ⟨ 1o , ∅ ⟩ ∈ ( 𝐴 ⊔ 1o ) ) → ( ( 𝐴 ⊔ 1o ) ∖ { 𝐵 } ) ≈ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) )
20 4 5 18 19 syl3anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → ( ( 𝐴 ⊔ 1o ) ∖ { 𝐵 } ) ≈ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) )
21 16 difeq1i ⊢ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) = ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ { ⟨ 1o , ∅ ⟩ } )
22 xp01disjl ⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 1o ) ) = ∅
23 disj3 ⊢ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 1o ) ) = ∅ ↔ ( { ∅ } × 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) ) )
24 22 23 mpbi ⊢ ( { ∅ } × 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) )
25 difun2 ⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ ( { 1o } × 1o ) ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) )
26 10 difeq2i ⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ ( { 1o } × 1o ) ) = ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ { ⟨ 1o , ∅ ⟩ } )
27 24 25 26 3eqtr2i ⊢ ( { ∅ } × 𝐴 ) = ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ { ⟨ 1o , ∅ ⟩ } )
28 21 27 eqtr4i ⊢ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) = ( { ∅ } × 𝐴 )
29 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
30 8 1 29 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
31 28 30 eqbrtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) ≈ 𝐴 )
32 entr ⊢ ( ( ( ( 𝐴 ⊔ 1o ) ∖ { 𝐵 } ) ≈ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) ∧ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) ≈ 𝐴 ) → ( ( 𝐴 ⊔ 1o ) ∖ { 𝐵 } ) ≈ 𝐴 )
33 20 31 32 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝐴 ⊔ 1o ) ) → ( ( 𝐴 ⊔ 1o ) ∖ { 𝐵 } ) ≈ 𝐴 )