Metamath Proof Explorer

Theorem ordtypelem2

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

Ref Expression
Hypotheses ordtypelem.1 ⊢F=recs⁡G
ordtypelem.2 ⊢C=w∈A|∀j∈ran⁡hjRw
ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
ordtypelem.5 ⊢T=x∈On|∃t∈A∀z∈FxzRt
ordtypelem.6 ⊢O=OrdIsoRA
ordtypelem.7 ⊢φ→RWeA
ordtypelem.8 ⊢φ→RSeA
Assertion ordtypelem2 ⊢φ→Ord⁡T

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢F=recs⁡G
2 ordtypelem.2 ⊢C=w∈A|∀j∈ran⁡hjRw
3 ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
4 ordtypelem.5 ⊢T=x∈On|∃t∈A∀z∈FxzRt
5 ordtypelem.6 ⊢O=OrdIsoRA
6 ordtypelem.7 ⊢φ→RWeA
7 ordtypelem.8 ⊢φ→RSeA
8 4 ssrab3 ⊢T⊆On
9 8 a1i ⊢φ→T⊆On
10 9 sselda ⊢φ∧a∈T→a∈On
11 onss ⊢a∈On→a⊆On
12 10 11 syl ⊢φ∧a∈T→a⊆On
13 eloni ⊢a∈On→Ord⁡a
14 10 13 syl ⊢φ∧a∈T→Ord⁡a
15 imaeq2 ⊢x=a→Fx=Fa
16 15 raleqdv ⊢x=a→∀z∈FxzRt↔∀z∈FazRt
17 16 rexbidv ⊢x=a→∃t∈A∀z∈FxzRt↔∃t∈A∀z∈FazRt
18 17 4 elrab2 ⊢a∈T↔a∈On∧∃t∈A∀z∈FazRt
19 18 simprbi ⊢a∈T→∃t∈A∀z∈FazRt
20 19 adantl ⊢φ∧a∈T→∃t∈A∀z∈FazRt
21 ordelss ⊢Ord⁡a∧x∈a→x⊆a
22 imass2 ⊢x⊆a→Fx⊆Fa
23 ssralv ⊢Fx⊆Fa→∀z∈FazRt→∀z∈FxzRt
24 23 reximdv ⊢Fx⊆Fa→∃t∈A∀z∈FazRt→∃t∈A∀z∈FxzRt
25 21 22 24 3syl ⊢Ord⁡a∧x∈a→∃t∈A∀z∈FazRt→∃t∈A∀z∈FxzRt
26 25 ralrimdva ⊢Ord⁡a→∃t∈A∀z∈FazRt→∀x∈a∃t∈A∀z∈FxzRt
27 14 20 26 sylc ⊢φ∧a∈T→∀x∈a∃t∈A∀z∈FxzRt
28 ssrab ⊢a⊆x∈On|∃t∈A∀z∈FxzRt↔a⊆On∧∀x∈a∃t∈A∀z∈FxzRt
29 12 27 28 sylanbrc ⊢φ∧a∈T→a⊆x∈On|∃t∈A∀z∈FxzRt
30 29 4 sseqtrrdi ⊢φ∧a∈T→a⊆T
31 30 ralrimiva ⊢φ→∀a∈Ta⊆T
32 dftr3 ⊢Tr⁡T↔∀a∈Ta⊆T
33 31 32 sylibr ⊢φ→Tr⁡T
34 ordon ⊢Ord⁡On
35 trssord ⊢Tr⁡T∧T⊆On∧Ord⁡On→Ord⁡T
36 8 34 35 mp3an23 ⊢Tr⁡T→Ord⁡T
37 33 36 syl ⊢φ→Ord⁡T