Metamath Proof Explorer

Theorem oicl

Description: The order type of the well-order R on A is an ordinal. (Contributed by Mario Carneiro, 23-May-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1 ⊢ F = OrdIso R A
Assertion oicl ⊢ Ord ⁡ dom ⁡ F

Proof

Step Hyp Ref Expression
1 oicl.1 ⊢ F = OrdIso R A
2 eqid ⊢ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
3 eqid ⊢ w ∈ A | ∀ j ∈ ran ⁡ h j R w = w ∈ A | ∀ j ∈ ran ⁡ h j R w
4 eqid ⊢ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v = h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
5 2 3 4 ordtypecbv ⊢ recs ⁡ f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s = recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
6 eqid ⊢ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s x z R t = x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ f ∈ V ⟼ ι s ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y | ∀ r ∈ y ∈ A | ∀ i ∈ ran ⁡ f i R y ¬ r R s x z R t
7 simpl ⊢ R We A ∧ R Se A → R We A
8 simpr ⊢ R We A ∧ R Se A → R Se A
9 5 3 4 6 1 7 8 ordtypelem5 ⊢ R We A ∧ R Se A → Ord ⁡ dom ⁡ F ∧ F : dom ⁡ F ⟶ A
10 9 simpld ⊢ R We A ∧ R Se A → Ord ⁡ dom ⁡ F
11 ord0 ⊢ Ord ⁡ ∅
12 1 oi0 ⊢ ¬ R We A ∧ R Se A → F = ∅
13 12 dmeqd ⊢ ¬ R We A ∧ R Se A → dom ⁡ F = dom ⁡ ∅
14 dm0 ⊢ dom ⁡ ∅ = ∅
15 13 14 eqtrdi ⊢ ¬ R We A ∧ R Se A → dom ⁡ F = ∅
16 ordeq ⊢ dom ⁡ F = ∅ → Ord ⁡ dom ⁡ F ↔ Ord ⁡ ∅
17 15 16 syl ⊢ ¬ R We A ∧ R Se A → Ord ⁡ dom ⁡ F ↔ Ord ⁡ ∅
18 11 17 mpbiri ⊢ ¬ R We A ∧ R Se A → Ord ⁡ dom ⁡ F
19 10 18 pm2.61i ⊢ Ord ⁡ dom ⁡ F