oieu

Description: Uniqueness of the unique ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015) (Revised by Mario Carneiro, 25-Jun-2015)

		Ref	Expression
	Hypothesis	oicl.1	$⊢ F = OrdIso (R, A)$
	Assertion	oieu	$⊢ (R We A \land R Se A) \to ((Ord B \land G {Isom}_{E, R} (B, A)) \leftrightarrow (B = dom F \land G = F))$

Proof

Step	Hyp	Ref	Expression
1		oicl.1	$⊢ F = OrdIso (R, A)$
2		simprr	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to G {Isom}_{E, R} (B, A)$
3	1	ordtype	$⊢ (R We A \land R Se A) \to F {Isom}_{E, R} (dom F, A)$
4	3	adantr	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to F {Isom}_{E, R} (dom F, A)$
5		isocnv	$⊢ F {Isom}_{E, R} (dom F, A) \to F^{-1} {Isom}_{R, E} (A, dom F)$
6	4 5	syl	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to F^{-1} {Isom}_{R, E} (A, dom F)$
7		isotr	$⊢ (G {Isom}_{E, R} (B, A) \land F^{-1} {Isom}_{R, E} (A, dom F)) \to (F^{-1} \circ G) {Isom}_{E, E} (B, dom F)$
8	2 6 7	syl2anc	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to (F^{-1} \circ G) {Isom}_{E, E} (B, dom F)$
9		simprl	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to Ord B$
10	1	oicl	$⊢ Ord dom F$
11	10	a1i	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to Ord dom F$
12		ordiso2	$⊢ ((F^{-1} \circ G) {Isom}_{E, E} (B, dom F) \land Ord B \land Ord dom F) \to B = dom F$
13	8 9 11 12	syl3anc	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to B = dom F$
14		ordwe	$⊢ Ord B \to E We B$
15	14	ad2antrl	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to E We B$
16		epse	$⊢ E Se B$
17	16	a1i	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to E Se B$
18		isoeq4	$⊢ B = dom F \to (F {Isom}_{E, R} (B, A) \leftrightarrow F {Isom}_{E, R} (dom F, A))$
19	13 18	syl	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to (F {Isom}_{E, R} (B, A) \leftrightarrow F {Isom}_{E, R} (dom F, A))$
20	4 19	mpbird	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to F {Isom}_{E, R} (B, A)$
21		weisoeq	$⊢ ((E We B \land E Se B) \land (G {Isom}_{E, R} (B, A) \land F {Isom}_{E, R} (B, A))) \to G = F$
22	15 17 2 20 21	syl22anc	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to G = F$
23	13 22	jca	$⊢ ((R We A \land R Se A) \land (Ord B \land G {Isom}_{E, R} (B, A))) \to (B = dom F \land G = F)$
24	23	ex	$⊢ (R We A \land R Se A) \to ((Ord B \land G {Isom}_{E, R} (B, A)) \to (B = dom F \land G = F))$
25	3 10	jctil	$⊢ (R We A \land R Se A) \to (Ord dom F \land F {Isom}_{E, R} (dom F, A))$
26		ordeq	$⊢ B = dom F \to (Ord B \leftrightarrow Ord dom F)$
27	26	adantr	$⊢ (B = dom F \land G = F) \to (Ord B \leftrightarrow Ord dom F)$
28		isoeq4	$⊢ B = dom F \to (G {Isom}_{E, R} (B, A) \leftrightarrow G {Isom}_{E, R} (dom F, A))$
29		isoeq1	$⊢ G = F \to (G {Isom}_{E, R} (dom F, A) \leftrightarrow F {Isom}_{E, R} (dom F, A))$
30	28 29	sylan9bb	$⊢ (B = dom F \land G = F) \to (G {Isom}_{E, R} (B, A) \leftrightarrow F {Isom}_{E, R} (dom F, A))$
31	27 30	anbi12d	$⊢ (B = dom F \land G = F) \to ((Ord B \land G {Isom}_{E, R} (B, A)) \leftrightarrow (Ord dom F \land F {Isom}_{E, R} (dom F, A)))$
32	25 31	syl5ibrcom	$⊢ (R We A \land R Se A) \to ((B = dom F \land G = F) \to (Ord B \land G {Isom}_{E, R} (B, A)))$
33	24 32	impbid	$⊢ (R We A \land R Se A) \to ((Ord B \land G {Isom}_{E, R} (B, A)) \leftrightarrow (B = dom F \land G = F))$

Metamath Proof Explorer

Theorem oieu

Proof