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		disjdifr	$⊢ (A ∖ \{X\}) \cap \{X\} = \emptyset$
7	6	a1i	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to (A ∖ \{X\}) \cap \{X\} = \emptyset$
8		nnord	$⊢ m \in ω \to Ord m$
9		ordirr	$⊢ Ord m \to \neg m \in m$
10	8 9	syl	$⊢ m \in ω \to \neg m \in m$
11		disjsn	$⊢ m \cap \{m\} = \emptyset \leftrightarrow \neg m \in m$
12	10 11	sylibr	$⊢ m \in ω \to m \cap \{m\} = \emptyset$
13	12	3ad2ant2	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to m \cap \{m\} = \emptyset$
14		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\})$
15	3 5 7 13 14	syl22anc	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to ((A ∖ \{X\}) \cup \{X\}) \approx (m \cup \{m\})$
16		difsnid	$⊢ X \in A \to (A ∖ \{X\}) \cup \{X\} = A$
17		df-suc	$⊢ suc m = m \cup \{m\}$
18	17	eqcomi	$⊢ m \cup \{m\} = suc m$
19	18	a1i	$⊢ X \in A \to m \cup \{m\} = suc m$
20	16 19	breq12d	$⊢ X \in A \to (((A ∖ \{X\}) \cup \{X\}) \approx (m \cup \{m\}) \leftrightarrow A \approx suc m)$
21	20	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)$
22	15 21	mpbid	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to A \approx suc m$
23		peano2	$⊢ m \in ω \to suc m \in ω$
24	23	3ad2ant2	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to suc m \in ω$
25		cardennn	$⊢ (A \approx suc m \land suc m \in ω) \to card (A) = suc m$
26	22 24 25	syl2anc	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to card (A) = suc m$
27		cardennn	$⊢ ((A ∖ \{X\}) \approx m \land m \in ω) \to card (A ∖ \{X\}) = m$
28	27	ancoms	$⊢ (m \in ω \land (A ∖ \{X\}) \approx m) \to card (A ∖ \{X\}) = m$
29	28	3adant1	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to card (A ∖ \{X\}) = m$
30		suceq	$⊢ card (A ∖ \{X\}) = m \to suc card (A ∖ \{X\}) = suc m$
31	29 30	syl	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to suc card (A ∖ \{X\}) = suc m$
32	26 31	eqtr4d	$⊢ (X \in A \land m \in ω \land (A ∖ \{X\}) \approx m) \to card (A) = suc card (A ∖ \{X\})$
33	32	3expib	$⊢ X \in A \to ((m \in ω \land (A ∖ \{X\}) \approx m) \to card (A) = suc card (A ∖ \{X\}))$
34	33	com12	$⊢ (m \in ω \land (A ∖ \{X\}) \approx m) \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
35	34	rexlimiva	$⊢ \exists m \in ω (A ∖ \{X\}) \approx m \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
36	2 35	sylbi	$⊢ A ∖ \{X\} \in Fin \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
37	1 36	syl	$⊢ A \in Fin \to (X \in A \to card (A) = suc card (A ∖ \{X\}))$
38	37	imp	$⊢ (A \in Fin \land X \in A) \to card (A) = suc card (A ∖ \{X\})$

Metamath Proof Explorer

Theorem dif1card

Proof