ordtypelem5

	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	ordtypelem5	$⊢ φ \to (Ord dom O \land O : dom O ⟶ A)$

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	ordtypelem2	$⊢ φ \to Ord T$
9	1	tfr1a	$⊢ (Fun F \land Lim dom F)$
10	9	simpri	$⊢ Lim dom F$
11		limord	$⊢ Lim dom F \to Ord dom F$
12	10 11	ax-mp	$⊢ Ord dom F$
13		ordin	$⊢ (Ord T \land Ord dom F) \to Ord (T \cap dom F)$
14	8 12 13	sylancl	$⊢ φ \to Ord (T \cap dom F)$
15	1 2 3 4 5 6 7	ordtypelem4	$⊢ φ \to O : T \cap dom F ⟶ A$
16	15	fdmd	$⊢ φ \to dom O = T \cap dom F$
17		ordeq	$⊢ dom O = T \cap dom F \to (Ord dom O \leftrightarrow Ord (T \cap dom F))$
18	16 17	syl	$⊢ φ \to (Ord dom O \leftrightarrow Ord (T \cap dom F))$
19	14 18	mpbird	$⊢ φ \to Ord dom O$
20	15	ffdmd	$⊢ φ \to O : dom O ⟶ A$
21	19 20	jca	$⊢ φ \to (Ord dom O \land O : dom O ⟶ A)$

Metamath Proof Explorer