ordtypelem8

	Ref	Expression
Hypotheses	ordtypelem.1	$⊢ F = recs (G)$
	ordtypelem.2	$⊢ C = \{w \in A \| \forall j \in ran h j R w\}$
	ordtypelem.3	$⊢ G = (h \in V ⟼ (ι v \in C \| \forall u \in C \neg u R v))$
	ordtypelem.5	$⊢ T = \{x \in On \| \exists t \in A \forall z \in F [x] z R t\}$
	ordtypelem.6	$⊢ O = OrdIso (R, A)$
	ordtypelem.7	$⊢ φ \to R We A$
	ordtypelem.8	$⊢ φ \to R Se A$
Assertion	ordtypelem8	$⊢ φ \to O {Isom}_{E, R} (dom O, ran O)$

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	$⊢ F = recs (G)$
2		ordtypelem.2	$⊢ C = \{w \in A \| \forall j \in ran h j R w\}$
3		ordtypelem.3	$⊢ G = (h \in V ⟼ (ι v \in C \| \forall u \in C \neg u R v))$
4		ordtypelem.5	$⊢ T = \{x \in On \| \exists t \in A \forall z \in F [x] z R t\}$
5		ordtypelem.6	$⊢ O = OrdIso (R, A)$
6		ordtypelem.7	$⊢ φ \to R We A$
7		ordtypelem.8	$⊢ φ \to R Se A$
8	1 2 3 4 5 6 7	ordtypelem4	$⊢ φ \to O : T \cap dom F ⟶ A$
9	8	fdmd	$⊢ φ \to dom O = T \cap dom F$
10		inss1	$⊢ T \cap dom F \subseteq T$
11	1 2 3 4 5 6 7	ordtypelem2	$⊢ φ \to Ord T$
12		ordsson	$⊢ Ord T \to T \subseteq On$
13	11 12	syl	$⊢ φ \to T \subseteq On$
14	10 13	sstrid	$⊢ φ \to T \cap dom F \subseteq On$
15	9 14	eqsstrd	$⊢ φ \to dom O \subseteq On$
16		epweon	$⊢ E We On$
17		weso	$⊢ E We On \to E Or On$
18	16 17	ax-mp	$⊢ E Or On$
19		soss	$⊢ dom O \subseteq On \to (E Or On \to E Or dom O)$
20	15 18 19	mpisyl	$⊢ φ \to E Or dom O$
21	8	frnd	$⊢ φ \to ran O \subseteq A$
22		wess	$⊢ ran O \subseteq A \to (R We A \to R We ran O)$
23	21 6 22	sylc	$⊢ φ \to R We ran O$
24		weso	$⊢ R We ran O \to R Or ran O$
25		sopo	$⊢ R Or ran O \to R Po ran O$
26	23 24 25	3syl	$⊢ φ \to R Po ran O$
27	8	ffund	$⊢ φ \to Fun O$
28		funforn	$⊢ Fun O \leftrightarrow O : dom O \underset{onto}{⟶} ran O$
29	27 28	sylib	$⊢ φ \to O : dom O \underset{onto}{⟶} ran O$
30		epel	$⊢ a E b \leftrightarrow a \in b$
31	1 2 3 4 5 6 7	ordtypelem6	$⊢ (φ \land b \in dom O) \to (a \in b \to O (a) R O (b))$
32	30 31	syl5bi	$⊢ (φ \land b \in dom O) \to (a E b \to O (a) R O (b))$
33	32	ralrimiva	$⊢ φ \to \forall b \in dom O (a E b \to O (a) R O (b))$
34	33	ralrimivw	$⊢ φ \to \forall a \in dom O \forall b \in dom O (a E b \to O (a) R O (b))$
35		soisoi	$⊢ ((E Or dom O \land R Po ran O) \land (O : dom O \underset{onto}{⟶} ran O \land \forall a \in dom O \forall b \in dom O (a E b \to O (a) R O (b)))) \to O {Isom}_{E, R} (dom O, ran O)$
36	20 26 29 34 35	syl22anc	$⊢ φ \to O {Isom}_{E, R} (dom O, ran O)$

Metamath Proof Explorer

Theorem ordtypelem8

Proof