MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-oi Structured version   Visualization version   GIF version

Definition df-oi 9278
Description: Define the canonical order isomorphism from the well-order 𝑅 on 𝐴 to an ordinal. (Contributed by Mario Carneiro, 23-May-2015.)
Assertion
Ref Expression
df-oi OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
Distinct variable groups:   ,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧,𝐴   𝑅,,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧

Detailed syntax breakdown of Definition df-oi
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2coi 9277 . 2 class OrdIso(𝑅, 𝐴)
41, 2wwe 5544 . . . 4 wff 𝑅 We 𝐴
51, 2wse 5543 . . . 4 wff 𝑅 Se 𝐴
64, 5wa 396 . . 3 wff (𝑅 We 𝐴𝑅 Se 𝐴)
7 vh . . . . . 6 setvar
8 cvv 3433 . . . . . 6 class V
9 vu . . . . . . . . . . 11 setvar 𝑢
109cv 1538 . . . . . . . . . 10 class 𝑢
11 vv . . . . . . . . . . 11 setvar 𝑣
1211cv 1538 . . . . . . . . . 10 class 𝑣
1310, 12, 2wbr 5075 . . . . . . . . 9 wff 𝑢𝑅𝑣
1413wn 3 . . . . . . . 8 wff ¬ 𝑢𝑅𝑣
15 vj . . . . . . . . . . . 12 setvar 𝑗
1615cv 1538 . . . . . . . . . . 11 class 𝑗
17 vw . . . . . . . . . . . 12 setvar 𝑤
1817cv 1538 . . . . . . . . . . 11 class 𝑤
1916, 18, 2wbr 5075 . . . . . . . . . 10 wff 𝑗𝑅𝑤
207cv 1538 . . . . . . . . . . 11 class
2120crn 5591 . . . . . . . . . 10 class ran
2219, 15, 21wral 3065 . . . . . . . . 9 wff 𝑗 ∈ ran 𝑗𝑅𝑤
2322, 17, 1crab 3069 . . . . . . . 8 class {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
2414, 9, 23wral 3065 . . . . . . 7 wff 𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣
2524, 11, 23crio 7240 . . . . . 6 class (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
267, 8, 25cmpt 5158 . . . . 5 class ( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
2726crecs 8210 . . . 4 class recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
28 vz . . . . . . . . 9 setvar 𝑧
2928cv 1538 . . . . . . . 8 class 𝑧
30 vt . . . . . . . . 9 setvar 𝑡
3130cv 1538 . . . . . . . 8 class 𝑡
3229, 31, 2wbr 5075 . . . . . . 7 wff 𝑧𝑅𝑡
33 vx . . . . . . . . 9 setvar 𝑥
3433cv 1538 . . . . . . . 8 class 𝑥
3527, 34cima 5593 . . . . . . 7 class (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)
3632, 28, 35wral 3065 . . . . . 6 wff 𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
3736, 30, 1wrex 3066 . . . . 5 wff 𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
38 con0 6270 . . . . 5 class On
3937, 33, 38crab 3069 . . . 4 class {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}
4027, 39cres 5592 . . 3 class (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡})
41 c0 4257 . . 3 class
426, 40, 41cif 4460 . 2 class if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
433, 42wceq 1539 1 wff OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
Colors of variables: wff setvar class
This definition is referenced by:  dfoi  9279  oieq1  9280  oieq2  9281  nfoi  9282  oi0  9296
  Copyright terms: Public domain W3C validator