oismo

Description: When A is a subclass of On , F is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of A ). The proof avoids ax-rep (the second statement is trivial under ax-rep ). (Contributed by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Hypothesis	oismo.1	$⊢ F = OrdIso (E, A)$
	Assertion	oismo	$⊢ A \subseteq On \to (Smo F \land ran F = A)$

Proof

Step	Hyp	Ref	Expression
1		oismo.1	$⊢ F = OrdIso (E, A)$
2		epweon	$⊢ E We On$
3		wess	$⊢ A \subseteq On \to (E We On \to E We A)$
4	2 3	mpi	$⊢ A \subseteq On \to E We A$
5		epse	$⊢ E Se A$
6	1	oiiso2	$⊢ (E We A \land E Se A) \to F {Isom}_{E, E} (dom F, ran F)$
7	4 5 6	sylancl	$⊢ A \subseteq On \to F {Isom}_{E, E} (dom F, ran F)$
8	1	oicl	$⊢ Ord dom F$
9	1	oif	$⊢ F : dom F ⟶ A$
10		frn	$⊢ F : dom F ⟶ A \to ran F \subseteq A$
11	9 10	ax-mp	$⊢ ran F \subseteq A$
12		id	$⊢ A \subseteq On \to A \subseteq On$
13	11 12	sstrid	$⊢ A \subseteq On \to ran F \subseteq On$
14		smoiso2	$⊢ (Ord dom F \land ran F \subseteq On) \to ((F : dom F \underset{onto}{⟶} ran F \land Smo F) \leftrightarrow F {Isom}_{E, E} (dom F, ran F))$
15	8 13 14	sylancr	$⊢ A \subseteq On \to ((F : dom F \underset{onto}{⟶} ran F \land Smo F) \leftrightarrow F {Isom}_{E, E} (dom F, ran F))$
16	7 15	mpbird	$⊢ A \subseteq On \to (F : dom F \underset{onto}{⟶} ran F \land Smo F)$
17	16	simprd	$⊢ A \subseteq On \to Smo F$
18	11	a1i	$⊢ A \subseteq On \to ran F \subseteq A$
19		simprl	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to x \in A$
20	4	adantr	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to E We A$
21	5	a1i	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to E Se A$
22		ffn	$⊢ F : dom F ⟶ A \to F Fn dom F$
23	9 22	mp1i	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to F Fn dom F$
24		simplrr	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to \neg x \in ran F$
25	4	ad2antrr	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to E We A$
26	5	a1i	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to E Se A$
27		simplrl	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to x \in A$
28		simpr	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to y \in dom F$
29	1	oiiniseg	$⊢ ((E We A \land E Se A) \land (x \in A \land y \in dom F)) \to (F (y) E x \lor x \in ran F)$
30	25 26 27 28 29	syl22anc	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to (F (y) E x \lor x \in ran F)$
31	30	ord	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to (\neg F (y) E x \to x \in ran F)$
32	24 31	mt3d	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to F (y) E x$
33		epel	$⊢ F (y) E x \leftrightarrow F (y) \in x$
34	32 33	sylib	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to F (y) \in x$
35	34	ralrimiva	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to \forall y \in dom F F (y) \in x$
36		ffnfv	$⊢ F : dom F ⟶ x \leftrightarrow (F Fn dom F \land \forall y \in dom F F (y) \in x)$
37	23 35 36	sylanbrc	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to F : dom F ⟶ x$
38	9 22	mp1i	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to F Fn dom F$
39	17	ad2antrr	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to Smo F$
40		smogt	$⊢ (F Fn dom F \land Smo F \land y \in dom F) \to y \subseteq F (y)$
41	38 39 28 40	syl3anc	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to y \subseteq F (y)$
42		ordelon	$⊢ (Ord dom F \land y \in dom F) \to y \in On$
43	8 28 42	sylancr	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to y \in On$
44		simpll	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to A \subseteq On$
45	44 27	sseldd	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to x \in On$
46		ontr2	$⊢ (y \in On \land x \in On) \to ((y \subseteq F (y) \land F (y) \in x) \to y \in x)$
47	43 45 46	syl2anc	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to ((y \subseteq F (y) \land F (y) \in x) \to y \in x)$
48	41 34 47	mp2and	$⊢ ((A \subseteq On \land (x \in A \land \neg x \in ran F)) \land y \in dom F) \to y \in x$
49	48	ex	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to (y \in dom F \to y \in x)$
50	49	ssrdv	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to dom F \subseteq x$
51	19 50	ssexd	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to dom F \in V$
52		fex2	$⊢ (F : dom F ⟶ x \land dom F \in V \land x \in A) \to F \in V$
53	37 51 19 52	syl3anc	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to F \in V$
54	1	ordtype2	$⊢ (E We A \land E Se A \land F \in V) \to F {Isom}_{E, E} (dom F, A)$
55	20 21 53 54	syl3anc	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to F {Isom}_{E, E} (dom F, A)$
56		isof1o	$⊢ F {Isom}_{E, E} (dom F, A) \to F : dom F \underset{1-1 onto}{⟶} A$
57		f1ofo	$⊢ F : dom F \underset{1-1 onto}{⟶} A \to F : dom F \underset{onto}{⟶} A$
58		forn	$⊢ F : dom F \underset{onto}{⟶} A \to ran F = A$
59	55 56 57 58	4syl	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to ran F = A$
60	19 59	eleqtrrd	$⊢ (A \subseteq On \land (x \in A \land \neg x \in ran F)) \to x \in ran F$
61	60	expr	$⊢ (A \subseteq On \land x \in A) \to (\neg x \in ran F \to x \in ran F)$
62	61	pm2.18d	$⊢ (A \subseteq On \land x \in A) \to x \in ran F$
63	18 62	eqelssd	$⊢ A \subseteq On \to ran F = A$
64	17 63	jca	$⊢ A \subseteq On \to (Smo F \land ran F = A)$

Metamath Proof Explorer

Theorem oismo

Proof