ordtypelem2

	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	ordtypelem2	⊢ ( 𝜑 → Ord 𝑇 )

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	4	ssrab3	⊢ 𝑇 ⊆ On
9	8	a1i	⊢ ( 𝜑 → 𝑇 ⊆ On )
10	9	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ On )
11		onss	⊢ ( 𝑎 ∈ On → 𝑎 ⊆ On )
12	10 11	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ⊆ On )
13		eloni	⊢ ( 𝑎 ∈ On → Ord 𝑎 )
14	10 13	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → Ord 𝑎 )
15		imaeq2	⊢ ( 𝑥 = 𝑎 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑎 ) )
16	15	raleqdv	⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 ) )
17	16	rexbidv	⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 ) )
18	17 4	elrab2	⊢ ( 𝑎 ∈ 𝑇 ↔ ( 𝑎 ∈ On ∧ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 ) )
19	18	simprbi	⊢ ( 𝑎 ∈ 𝑇 → ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 )
21		ordelss	⊢ ( ( Ord 𝑎 ∧ 𝑥 ∈ 𝑎 ) → 𝑥 ⊆ 𝑎 )
22		imass2	⊢ ( 𝑥 ⊆ 𝑎 → ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑎 ) )
23		ssralv	⊢ ( ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑎 ) → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 → ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ) )
24	23	reximdv	⊢ ( ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑎 ) → ( ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 → ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ) )
25	21 22 24	3syl	⊢ ( ( Ord 𝑎 ∧ 𝑥 ∈ 𝑎 ) → ( ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 → ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ) )
26	25	ralrimdva	⊢ ( Ord 𝑎 → ( ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑎 ) 𝑧 𝑅 𝑡 → ∀ 𝑥 ∈ 𝑎 ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ) )
27	14 20 26	sylc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ∀ 𝑥 ∈ 𝑎 ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 )
28		ssrab	⊢ ( 𝑎 ⊆ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } ↔ ( 𝑎 ⊆ On ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ) )
29	12 27 28	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ⊆ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } )
30	29 4	sseqtrrdi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ⊆ 𝑇 )
31	30	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑇 𝑎 ⊆ 𝑇 )
32		dftr3	⊢ ( Tr 𝑇 ↔ ∀ 𝑎 ∈ 𝑇 𝑎 ⊆ 𝑇 )
33	31 32	sylibr	⊢ ( 𝜑 → Tr 𝑇 )
34		ordon	⊢ Ord On
35		trssord	⊢ ( ( Tr 𝑇 ∧ 𝑇 ⊆ On ∧ Ord On ) → Ord 𝑇 )
36	8 34 35	mp3an23	⊢ ( Tr 𝑇 → Ord 𝑇 )
37	33 36	syl	⊢ ( 𝜑 → Ord 𝑇 )

Metamath Proof Explorer

Theorem ordtypelem2

Proof