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 ) ∖ { 𝐵 } ) ≈ 𝐴 )