finnisoeu

Description: A finite totally ordered set has a unique order isomorphism to a finite ordinal. (Contributed by Stefan O'Rear, 16-Nov-2014) (Proof shortened by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	finnisoeu	$⊢ (R Or A \land A \in Fin) \to \exists! f f {Isom}_{E, R} (card (A), A)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ OrdIso (R, A) = OrdIso (R, A)$
2	1	oiexg	$⊢ A \in Fin \to OrdIso (R, A) \in V$
3	2	adantl	$⊢ (R Or A \land A \in Fin) \to OrdIso (R, A) \in V$
4		simpr	$⊢ (R Or A \land A \in Fin) \to A \in Fin$
5		wofi	$⊢ (R Or A \land A \in Fin) \to R We A$
6	1	oiiso	$⊢ (A \in Fin \land R We A) \to OrdIso (R, A) {Isom}_{E, R} (dom OrdIso (R, A), A)$
7	4 5 6	syl2anc	$⊢ (R Or A \land A \in Fin) \to OrdIso (R, A) {Isom}_{E, R} (dom OrdIso (R, A), A)$
8	1	oien	$⊢ (A \in Fin \land R We A) \to dom OrdIso (R, A) \approx A$
9	4 5 8	syl2anc	$⊢ (R Or A \land A \in Fin) \to dom OrdIso (R, A) \approx A$
10		ficardid	$⊢ A \in Fin \to card (A) \approx A$
11	10	adantl	$⊢ (R Or A \land A \in Fin) \to card (A) \approx A$
12	11	ensymd	$⊢ (R Or A \land A \in Fin) \to A \approx card (A)$
13		entr	$⊢ (dom OrdIso (R, A) \approx A \land A \approx card (A)) \to dom OrdIso (R, A) \approx card (A)$
14	9 12 13	syl2anc	$⊢ (R Or A \land A \in Fin) \to dom OrdIso (R, A) \approx card (A)$
15	1	oion	$⊢ A \in Fin \to dom OrdIso (R, A) \in On$
16	15	adantl	$⊢ (R Or A \land A \in Fin) \to dom OrdIso (R, A) \in On$
17		ficardom	$⊢ A \in Fin \to card (A) \in ω$
18	17	adantl	$⊢ (R Or A \land A \in Fin) \to card (A) \in ω$
19		onomeneq	$⊢ (dom OrdIso (R, A) \in On \land card (A) \in ω) \to (dom OrdIso (R, A) \approx card (A) \leftrightarrow dom OrdIso (R, A) = card (A))$
20	16 18 19	syl2anc	$⊢ (R Or A \land A \in Fin) \to (dom OrdIso (R, A) \approx card (A) \leftrightarrow dom OrdIso (R, A) = card (A))$
21	14 20	mpbid	$⊢ (R Or A \land A \in Fin) \to dom OrdIso (R, A) = card (A)$
22		isoeq4	$⊢ dom OrdIso (R, A) = card (A) \to (OrdIso (R, A) {Isom}_{E, R} (dom OrdIso (R, A), A) \leftrightarrow OrdIso (R, A) {Isom}_{E, R} (card (A), A))$
23	21 22	syl	$⊢ (R Or A \land A \in Fin) \to (OrdIso (R, A) {Isom}_{E, R} (dom OrdIso (R, A), A) \leftrightarrow OrdIso (R, A) {Isom}_{E, R} (card (A), A))$
24	7 23	mpbid	$⊢ (R Or A \land A \in Fin) \to OrdIso (R, A) {Isom}_{E, R} (card (A), A)$
25		isoeq1	$⊢ f = OrdIso (R, A) \to (f {Isom}_{E, R} (card (A), A) \leftrightarrow OrdIso (R, A) {Isom}_{E, R} (card (A), A))$
26	3 24 25	spcedv	$⊢ (R Or A \land A \in Fin) \to \exists f f {Isom}_{E, R} (card (A), A)$
27		wemoiso2	$⊢ R We A \to \exists^{*} f f {Isom}_{E, R} (card (A), A)$
28	5 27	syl	$⊢ (R Or A \land A \in Fin) \to \exists^{*} f f {Isom}_{E, R} (card (A), A)$
29		df-eu	$⊢ \exists! f f {Isom}_{E, R} (card (A), A) \leftrightarrow (\exists f f {Isom}_{E, R} (card (A), A) \land \exists^{*} f f {Isom}_{E, R} (card (A), A))$
30	26 28 29	sylanbrc	$⊢ (R Or A \land A \in Fin) \to \exists! f f {Isom}_{E, R} (card (A), A)$

Metamath Proof Explorer

Theorem finnisoeu

Proof