Metamath Proof Explorer

Theorem ordtypelem1

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 ⁡ h j R w
ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
ordtypelem.5 ⊢ T = x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
ordtypelem.6 ⊢ O = OrdIso R A
ordtypelem.7 ⊢ φ → R We A
ordtypelem.8 ⊢ φ → R Se A
Assertion ordtypelem1 ⊢ φ → O = F ↾ T

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢ F = recs ⁡ G
2 ordtypelem.2 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
3 ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
4 ordtypelem.5 ⊢ T = x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
5 ordtypelem.6 ⊢ O = OrdIso R A
6 ordtypelem.7 ⊢ φ → R We A
7 ordtypelem.8 ⊢ φ → R Se A
8 iftrue ⊢ R We A ∧ R Se A → if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅ = F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
9 6 7 8 syl2anc ⊢ φ → if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅ = F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
10 2 3 1 dfoi ⊢ OrdIso R A = if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅
11 5 10 eqtri ⊢ O = if R We A ∧ R Se A F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t ∅
12 4 reseq2i ⊢ F ↾ T = F ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
13 9 11 12 3eqtr4g ⊢ φ → O = F ↾ T