ordtypelem6

	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	ordtypelem6	$⊢ (φ \land M \in dom O) \to (N \in M \to O (N) R O (M))$

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		fveq2	$⊢ a = N \to F (a) = F (N)$
9	8	breq1d	$⊢ a = N \to (F (a) R F (M) \leftrightarrow F (N) R F (M))$
10		ssrab2	$⊢ \{v \in \{w \in A \| \forall j \in F [M] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [M] j R w\} \neg u R v\} \subseteq \{w \in A \| \forall j \in F [M] j R w\}$
11		simpr	$⊢ (φ \land M \in dom O) \to M \in dom O$
12	1 2 3 4 5 6 7	ordtypelem4	$⊢ φ \to O : T \cap dom F ⟶ A$
13	12	fdmd	$⊢ φ \to dom O = T \cap dom F$
14	13	adantr	$⊢ (φ \land M \in dom O) \to dom O = T \cap dom F$
15	11 14	eleqtrd	$⊢ (φ \land M \in dom O) \to M \in (T \cap dom F)$
16	1 2 3 4 5 6 7	ordtypelem3	$⊢ (φ \land M \in (T \cap dom F)) \to F (M) \in \{v \in \{w \in A \| \forall j \in F [M] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [M] j R w\} \neg u R v\}$
17	15 16	syldan	$⊢ (φ \land M \in dom O) \to F (M) \in \{v \in \{w \in A \| \forall j \in F [M] j R w\} \| \forall u \in \{w \in A \| \forall j \in F [M] j R w\} \neg u R v\}$
18	10 17	sselid	$⊢ (φ \land M \in dom O) \to F (M) \in \{w \in A \| \forall j \in F [M] j R w\}$
19		breq2	$⊢ w = F (M) \to (j R w \leftrightarrow j R F (M))$
20	19	ralbidv	$⊢ w = F (M) \to (\forall j \in F [M] j R w \leftrightarrow \forall j \in F [M] j R F (M))$
21	20	elrab	$⊢ F (M) \in \{w \in A \| \forall j \in F [M] j R w\} \leftrightarrow (F (M) \in A \land \forall j \in F [M] j R F (M))$
22	21	simprbi	$⊢ F (M) \in \{w \in A \| \forall j \in F [M] j R w\} \to \forall j \in F [M] j R F (M)$
23	18 22	syl	$⊢ (φ \land M \in dom O) \to \forall j \in F [M] j R F (M)$
24	1	tfr1a	$⊢ (Fun F \land Lim dom F)$
25	24	simpli	$⊢ Fun F$
26		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
27	25 26	mpbi	$⊢ F Fn dom F$
28	24	simpri	$⊢ Lim dom F$
29		limord	$⊢ Lim dom F \to Ord dom F$
30	28 29	ax-mp	$⊢ Ord dom F$
31		inss2	$⊢ T \cap dom F \subseteq dom F$
32	13 31	eqsstrdi	$⊢ φ \to dom O \subseteq dom F$
33	32	sselda	$⊢ (φ \land M \in dom O) \to M \in dom F$
34		ordelss	$⊢ (Ord dom F \land M \in dom F) \to M \subseteq dom F$
35	30 33 34	sylancr	$⊢ (φ \land M \in dom O) \to M \subseteq dom F$
36		breq1	$⊢ j = F (a) \to (j R F (M) \leftrightarrow F (a) R F (M))$
37	36	ralima	$⊢ (F Fn dom F \land M \subseteq dom F) \to (\forall j \in F [M] j R F (M) \leftrightarrow \forall a \in M F (a) R F (M))$
38	27 35 37	sylancr	$⊢ (φ \land M \in dom O) \to (\forall j \in F [M] j R F (M) \leftrightarrow \forall a \in M F (a) R F (M))$
39	23 38	mpbid	$⊢ (φ \land M \in dom O) \to \forall a \in M F (a) R F (M)$
40	39	adantrr	$⊢ (φ \land (M \in dom O \land N \in M)) \to \forall a \in M F (a) R F (M)$
41		simprr	$⊢ (φ \land (M \in dom O \land N \in M)) \to N \in M$
42	9 40 41	rspcdva	$⊢ (φ \land (M \in dom O \land N \in M)) \to F (N) R F (M)$
43	1 2 3 4 5 6 7	ordtypelem1	$⊢ φ \to O = {F ↾}_{T}$
44	43	adantr	$⊢ (φ \land (M \in dom O \land N \in M)) \to O = {F ↾}_{T}$
45	44	fveq1d	$⊢ (φ \land (M \in dom O \land N \in M)) \to O (N) = ({F ↾}_{T}) (N)$
46	1 2 3 4 5 6 7	ordtypelem2	$⊢ φ \to Ord T$
47		inss1	$⊢ T \cap dom F \subseteq T$
48	13 47	eqsstrdi	$⊢ φ \to dom O \subseteq T$
49	48	sselda	$⊢ (φ \land M \in dom O) \to M \in T$
50	49	adantrr	$⊢ (φ \land (M \in dom O \land N \in M)) \to M \in T$
51		ordelss	$⊢ (Ord T \land M \in T) \to M \subseteq T$
52	46 50 51	syl2an2r	$⊢ (φ \land (M \in dom O \land N \in M)) \to M \subseteq T$
53	52 41	sseldd	$⊢ (φ \land (M \in dom O \land N \in M)) \to N \in T$
54	53	fvresd	$⊢ (φ \land (M \in dom O \land N \in M)) \to ({F ↾}_{T}) (N) = F (N)$
55	45 54	eqtrd	$⊢ (φ \land (M \in dom O \land N \in M)) \to O (N) = F (N)$
56	44	fveq1d	$⊢ (φ \land (M \in dom O \land N \in M)) \to O (M) = ({F ↾}_{T}) (M)$
57	50	fvresd	$⊢ (φ \land (M \in dom O \land N \in M)) \to ({F ↾}_{T}) (M) = F (M)$
58	56 57	eqtrd	$⊢ (φ \land (M \in dom O \land N \in M)) \to O (M) = F (M)$
59	42 55 58	3brtr4d	$⊢ (φ \land (M \in dom O \land N \in M)) \to O (N) R O (M)$
60	59	expr	$⊢ (φ \land M \in dom O) \to (N \in M \to O (N) R O (M))$

Metamath Proof Explorer

Theorem ordtypelem6

Proof