Theorem ordtypelem6

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Hypotheses	ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
	ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
	ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
	ordtypelem.5	⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
	ordtypelem.6	⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
	ordtypelem.7	⊢ ( 𝜑 → 𝑅 We 𝐴 )
	ordtypelem.8	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
Assertion	ordtypelem6	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝑁 ∈ 𝑀 → ( 𝑂 ‘ 𝑁 ) 𝑅 ( 𝑂 ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
2		ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
3		ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
4		ordtypelem.5	⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
5		ordtypelem.6	⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
6		ordtypelem.7	⊢ ( 𝜑 → 𝑅 We 𝐴 )
7		ordtypelem.8	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
8		fveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑁 ) )
9	8	breq1d	⊢ ( 𝑎 = 𝑁 → ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ( 𝐹 ‘ 𝑁 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
10		ssrab2	⊢ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ⊆ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 }
11		simpr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ dom 𝑂 )
12	1 2 3 4 5 6 7	ordtypelem4	⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
13	12	fdmd	⊢ ( 𝜑 → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
15	11 14	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) )
16	1 2 3 4 5 6 7	ordtypelem3	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
17	15 16	syldan	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
18	10 17	sseldi	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } )
19		breq2	⊢ ( 𝑤 = ( 𝐹 ‘ 𝑀 ) → ( 𝑗 𝑅 𝑤 ↔ 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
20	19	ralbidv	⊢ ( 𝑤 = ( 𝐹 ‘ 𝑀 ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ↔ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
21	20	elrab	⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ↔ ( ( 𝐹 ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
22	21	simprbi	⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } → ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) )
23	18 22	syl	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) )
24	1	tfr1a	⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 )
25	24	simpli	⊢ Fun 𝐹
26		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
27	25 26	mpbi	⊢ 𝐹 Fn dom 𝐹
28	24	simpri	⊢ Lim dom 𝐹
29		limord	⊢ ( Lim dom 𝐹 → Ord dom 𝐹 )
30	28 29	ax-mp	⊢ Ord dom 𝐹
31		inss2	⊢ ( 𝑇 ∩ dom 𝐹 ) ⊆ dom 𝐹
32	13 31	eqsstrdi	⊢ ( 𝜑 → dom 𝑂 ⊆ dom 𝐹 )
33	32	sselda	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ dom 𝐹 )
34		ordelss	⊢ ( ( Ord dom 𝐹 ∧ 𝑀 ∈ dom 𝐹 ) → 𝑀 ⊆ dom 𝐹 )
35	30 33 34	sylancr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ⊆ dom 𝐹 )
36		breq1	⊢ ( 𝑗 = ( 𝐹 ‘ 𝑎 ) → ( 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
37	36	ralima	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑀 ⊆ dom 𝐹 ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
38	27 35 37	sylancr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
39	23 38	mpbid	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) )
40	39	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) )
41		simprr	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑁 ∈ 𝑀 )
42	9 40 41	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝐹 ‘ 𝑁 ) 𝑅 ( 𝐹 ‘ 𝑀 ) )
43	1 2 3 4 5 6 7	ordtypelem1	⊢ ( 𝜑 → 𝑂 = ( 𝐹 ↾ 𝑇 ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑂 = ( 𝐹 ↾ 𝑇 ) )
45	44	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑁 ) = ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑁 ) )
46	1 2 3 4 5 6 7	ordtypelem2	⊢ ( 𝜑 → Ord 𝑇 )
47		inss1	⊢ ( 𝑇 ∩ dom 𝐹 ) ⊆ 𝑇
48	13 47	eqsstrdi	⊢ ( 𝜑 → dom 𝑂 ⊆ 𝑇 )
49	48	sselda	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ 𝑇 )
50	49	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑀 ∈ 𝑇 )
51		ordelss	⊢ ( ( Ord 𝑇 ∧ 𝑀 ∈ 𝑇 ) → 𝑀 ⊆ 𝑇 )
52	46 50 51	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑀 ⊆ 𝑇 )
53	52 41	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑁 ∈ 𝑇 )
54	53	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
55	45 54	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
56	44	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑀 ) = ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑀 ) )
57	50	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
58	56 57	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
59	42 55 58	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑁 ) 𝑅 ( 𝑂 ‘ 𝑀 ) )
60	59	expr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝑁 ∈ 𝑀 → ( 𝑂 ‘ 𝑁 ) 𝑅 ( 𝑂 ‘ 𝑀 ) ) )