dif1card

Description: The cardinality of a nonempty finite set is one greater than the cardinality of the set with one element removed. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 2-Feb-2013)

		Ref	Expression
	Assertion	dif1card	$⊢ (A \in Fin \land X \in A) \to card (A) = suc card (A ∖ \{X\})$

Proof

Step	Hyp	Ref	Expression
1		diffi	$⊢ A \in Fin \to A ∖ \{X\} \in Fin$
2		isfi	$⊢ A ∖ \{X\} \in Fin \leftrightarrow \exists m \in ω (A ∖ \{X\}) \approx m$
3		simp3	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to (A ∖ \{X\}) \approx m$
4		en2sn	$⊢ (X \in A \land m \in ω) \to \{X\} \approx \{m\}$
5	4	3adant3	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to \{X\} \approx \{m\}$
6		incom	$⊢ (A ∖ \{X\}) \cap \{X\} = \{X\} \cap (A ∖ \{X\})$
7		disjdif	$⊢ \{X\} \cap (A ∖ \{X\}) = \emptyset$
8	6 7	eqtri	$⊢ (A ∖ \{X\}) \cap \{X\} = \emptyset$
9	8	a1i	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to (A ∖ \{X\}) \cap \{X\} = \emptyset$
10		nnord	$⊢ m \in ω \to Ord m$
11		ordirr	$⊢ Ord m \to \neg m \in m$
12	10 11	syl	$⊢ m \in ω \to \neg m \in m$
13		disjsn	$⊢ m \cap \{m\} = \emptyset \leftrightarrow \neg m \in m$
14	12 13	sylibr	$⊢ m \in ω \to m \cap \{m\} = \emptyset$
15	14	3ad2ant2	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to m \cap \{m\} = \emptyset$
16		unen	$⊢ (((A ∖ \{X\}) \approx m \land \{X\} \approx \{m\}) \land ((A ∖ \{X\}) \cap \{X\} = \emptyset \land m \cap \{m\} = \emptyset)) \to ((A ∖ \{X\}) \cup \{X\}) \approx (m \cup \{m\})$
17	3 5 9 15 16	syl22anc	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to ((A ∖ \{X\}) \cup \{X\}) \approx (m \cup \{m\})$
18		difsnid	$⊢ X \in A \to (A ∖ \{X\}) \cup \{X\} = A$
19		df-suc	$⊢ suc m = m \cup \{m\}$
20	19	eqcomi	$⊢ m \cup \{m\} = suc m$
21	20	a1i	$⊢ X \in A \to m \cup \{m\} = suc m$
22	18 21	breq12d	$⊢ X \in A \to (((A ∖ \{X\}) \cup \{X\}) \approx (m \cup \{m\}) \leftrightarrow A \approx suc m)$
23	22	3ad2ant1	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to (((A ∖ \{X\}) \cup \{X\}) \approx (m \cup \{m\}) \leftrightarrow A \approx suc m)$
24	17 23	mpbid	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to A \approx suc m$
25		peano2	$⊢ m \in ω \to suc m \in ω$
26	25	3ad2ant2	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to suc m \in ω$
27		cardennn	$⊢ (A \approx suc m \land suc m \in ω) \to card (A) = suc m$
28	24 26 27	syl2anc	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to card (A) = suc m$
29		cardennn	$⊢ ((A ∖ \{X\}) \approx m \land m \in ω) \to card (A ∖ \{X\}) = m$
30	29	ancoms	$⊢ (m \in ω \land (A ∖ \{X\}) \approx m) \to card (A ∖ \{X\}) = m$
31	30	3adant1	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to card (A ∖ \{X\}) = m$
32		suceq	$⊢ card (A ∖ \{X\}) = m \to suc card (A ∖ \{X\}) = suc m$
33	31 32	syl	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to suc card (A ∖ \{X\}) = suc m$
34	28 33	eqtr4d	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to card (A) = suc card (A ∖ \{X\})$
35	34	3expib	$⊢ X \in A \to ((m \in ω \land (A ∖ \{X\}) \approx m) \to card (A) = suc card (A ∖ \{X\}))$
36	35	com12	$⊢ (m \in ω \land (A ∖ \{X\}) \approx m) \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
37	36	rexlimiva	$⊢ \exists m \in ω (A ∖ \{X\}) \approx m \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
38	2 37	sylbi	$⊢ A ∖ \{X\} \in Fin \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
39	1 38	syl	$⊢ A \in Fin \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
40	39	imp	$⊢ (A \in Fin \land X \in A) \to card (A) = suc card (A ∖ \{X\})$

Metamath Proof Explorer

Theorem dif1card

Proof