Metamath Proof Explorer

Theorem ordtypelem4

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 ordtypelem4 ⊢φ→O:T∩dom⁡F⟶A

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 1 tfr1a ⊢Fun⁡F∧Lim⁡dom⁡F
9 8 simpli ⊢Fun⁡F
10 funres ⊢Fun⁡F→Fun⁡F↾T
11 9 10 mp1i ⊢φ→Fun⁡F↾T
12 11 funfnd ⊢φ→F↾TFndom⁡F↾T
13 dmres ⊢dom⁡F↾T=T∩dom⁡F
14 13 fneq2i ⊢F↾TFndom⁡F↾T↔F↾TFnT∩dom⁡F
15 12 14 sylib ⊢φ→F↾TFnT∩dom⁡F
16 simpr ⊢φ∧a∈T∩dom⁡F→a∈T∩dom⁡F
17 16 elin1d ⊢φ∧a∈T∩dom⁡F→a∈T
18 17 fvresd ⊢φ∧a∈T∩dom⁡F→F↾T⁡a=F⁡a
19 ssrab2 ⊢v∈w∈A|∀j∈FajRw|∀u∈w∈A|∀j∈FajRw¬uRv⊆w∈A|∀j∈FajRw
20 ssrab2 ⊢w∈A|∀j∈FajRw⊆A
21 19 20 sstri ⊢v∈w∈A|∀j∈FajRw|∀u∈w∈A|∀j∈FajRw¬uRv⊆A
22 1 2 3 4 5 6 7 ordtypelem3 ⊢φ∧a∈T∩dom⁡F→F⁡a∈v∈w∈A|∀j∈FajRw|∀u∈w∈A|∀j∈FajRw¬uRv
23 21 22 sselid ⊢φ∧a∈T∩dom⁡F→F⁡a∈A
24 18 23 eqeltrd ⊢φ∧a∈T∩dom⁡F→F↾T⁡a∈A
25 24 ralrimiva ⊢φ→∀a∈T∩dom⁡FF↾T⁡a∈A
26 ffnfv ⊢F↾T:T∩dom⁡F⟶A↔F↾TFnT∩dom⁡F∧∀a∈T∩dom⁡FF↾T⁡a∈A
27 15 25 26 sylanbrc ⊢φ→F↾T:T∩dom⁡F⟶A
28 1 2 3 4 5 6 7 ordtypelem1 ⊢φ→O=F↾T
29 28 feq1d ⊢φ→O:T∩dom⁡F⟶A↔F↾T:T∩dom⁡F⟶A
30 27 29 mpbird ⊢φ→O:T∩dom⁡F⟶A