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 \in V \land B \in (A ⊔︀ 1_{𝑜})) \to ((A ⊔︀ 1_{𝑜}) ∖ \{B\}) \approx A$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to A \in V$
2		1oex	$⊢ 1_{𝑜} \in V$
3		djuex	$⊢ (A \in V \land 1_{𝑜} \in V) \to (A ⊔︀ 1_{𝑜}) \in V$
4	1 2 3	sylancl	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to (A ⊔︀ 1_{𝑜}) \in V$
5		simpr	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to B \in (A ⊔︀ 1_{𝑜})$
6		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
7	6	xpeq2i	$⊢ \{1_{𝑜}\} \times 1_{𝑜} = \{1_{𝑜}\} \times \{\emptyset\}$
8		0ex	$⊢ \emptyset \in V$
9	2 8	xpsn	$⊢ \{1_{𝑜}\} \times \{\emptyset\} = \{⟨1_{𝑜}, \emptyset⟩\}$
10	7 9	eqtri	$⊢ \{1_{𝑜}\} \times 1_{𝑜} = \{⟨1_{𝑜}, \emptyset⟩\}$
11		ssun2	$⊢ \{1_{𝑜}\} \times 1_{𝑜} \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})$
12	10 11	eqsstrri	$⊢ \{⟨1_{𝑜}, \emptyset⟩\} \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})$
13		opex	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in V$
14	13	snss	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})) \leftrightarrow \{⟨1_{𝑜}, \emptyset⟩\} \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})$
15	12 14	mpbir	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}))$
16		df-dju	$⊢ (A ⊔︀ 1_{𝑜}) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})$
17	15 16	eleqtrri	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in (A ⊔︀ 1_{𝑜})$
18	17	a1i	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to ⟨1_{𝑜}, \emptyset⟩ \in (A ⊔︀ 1_{𝑜})$
19		difsnen	$⊢ ((A ⊔︀ 1_{𝑜}) \in V \land B \in (A ⊔︀ 1_{𝑜}) \land ⟨1_{𝑜}, \emptyset⟩ \in (A ⊔︀ 1_{𝑜})) \to ((A ⊔︀ 1_{𝑜}) ∖ \{B\}) \approx ((A ⊔︀ 1_{𝑜}) ∖ \{⟨1_{𝑜}, \emptyset⟩\})$
20	4 5 18 19	syl3anc	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to ((A ⊔︀ 1_{𝑜}) ∖ \{B\}) \approx ((A ⊔︀ 1_{𝑜}) ∖ \{⟨1_{𝑜}, \emptyset⟩\})$
21	16	difeq1i	$⊢ (A ⊔︀ 1_{𝑜}) ∖ \{⟨1_{𝑜}, \emptyset⟩\} = ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})) ∖ \{⟨1_{𝑜}, \emptyset⟩\}$
22		xp01disjl	$⊢ (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times 1_{𝑜}) = \emptyset$
23		disj3	$⊢ (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times 1_{𝑜}) = \emptyset \leftrightarrow \{\emptyset\} \times A = (\{\emptyset\} \times A) ∖ (\{1_{𝑜}\} \times 1_{𝑜})$
24	22 23	mpbi	$⊢ \{\emptyset\} \times A = (\{\emptyset\} \times A) ∖ (\{1_{𝑜}\} \times 1_{𝑜})$
25		difun2	$⊢ ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})) ∖ (\{1_{𝑜}\} \times 1_{𝑜}) = (\{\emptyset\} \times A) ∖ (\{1_{𝑜}\} \times 1_{𝑜})$
26	10	difeq2i	$⊢ ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})) ∖ (\{1_{𝑜}\} \times 1_{𝑜}) = ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})) ∖ \{⟨1_{𝑜}, \emptyset⟩\}$
27	24 25 26	3eqtr2i	$⊢ \{\emptyset\} \times A = ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})) ∖ \{⟨1_{𝑜}, \emptyset⟩\}$
28	21 27	eqtr4i	$⊢ (A ⊔︀ 1_{𝑜}) ∖ \{⟨1_{𝑜}, \emptyset⟩\} = \{\emptyset\} \times A$
29		xpsnen2g	$⊢ (\emptyset \in V \land A \in V) \to (\{\emptyset\} \times A) \approx A$
30	8 1 29	sylancr	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to (\{\emptyset\} \times A) \approx A$
31	28 30	eqbrtrid	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to ((A ⊔︀ 1_{𝑜}) ∖ \{⟨1_{𝑜}, \emptyset⟩\}) \approx A$
32		entr	$⊢ (((A ⊔︀ 1_{𝑜}) ∖ \{B\}) \approx ((A ⊔︀ 1_{𝑜}) ∖ \{⟨1_{𝑜}, \emptyset⟩\}) \land ((A ⊔︀ 1_{𝑜}) ∖ \{⟨1_{𝑜}, \emptyset⟩\}) \approx A) \to ((A ⊔︀ 1_{𝑜}) ∖ \{B\}) \approx A$
33	20 31 32	syl2anc	$⊢ (A \in V \land B \in (A ⊔︀ 1_{𝑜})) \to ((A ⊔︀ 1_{𝑜}) ∖ \{B\}) \approx A$

Metamath Proof Explorer

Theorem dju1dif

Proof