Metamath Proof Explorer

Definition df-oi

Description: Define the canonical order isomorphism from the well-order R on A to an ordinal. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Assertion df-oi ⊢ OrdIso R A = if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 cA class A
2 1 0 coi class OrdIso R A
3 1 0 wwe wff R We A
4 1 0 wse wff R Se A
5 3 4 wa wff R We A ∧ R Se A
6 vh setvar h
7 cvv class V
8 vv setvar v
9 vw setvar w
10 vj setvar j
11 6 cv setvar h
12 11 crn class ran ⁡ h
13 10 cv setvar j
14 9 cv setvar w
15 13 14 0 wbr wff j R w
16 15 10 12 wral wff ∀ j ∈ ran ⁡ h j R w
17 16 9 1 crab class w ∈ A | ∀ j ∈ ran ⁡ h j R w
18 vu setvar u
19 18 cv setvar u
20 8 cv setvar v
21 19 20 0 wbr wff u R v
22 21 wn wff ¬ u R v
23 22 18 17 wral wff ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
24 23 8 17 crio class ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
25 6 7 24 cmpt class h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
26 25 crecs class recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v
27 vx setvar x
28 con0 class On
29 vt setvar t
30 vz setvar z
31 27 cv setvar x
32 26 31 cima class recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x
33 30 cv setvar z
34 29 cv setvar t
35 33 34 0 wbr wff z R t
36 35 30 32 wral wff ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
37 36 29 1 wrex wff ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
38 37 27 28 crab class x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
39 26 38 cres class recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t
40 c0 class ∅
41 5 39 40 cif class if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅
42 2 41 wceq wff OrdIso R A = if R We A ∧ R Se A recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v ↾ x ∈ On | ∃ t ∈ A ∀ z ∈ recs ⁡ h ∈ V ⟼ ι v ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w | ∀ u ∈ w ∈ A | ∀ j ∈ ran ⁡ h j R w ¬ u R v x z R t ∅