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 9050
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 9049 . 2 class OrdIso(𝑅, 𝐴)
41, 2wwe 5483 . . . 4 wff 𝑅 We 𝐴
51, 2wse 5482 . . . 4 wff 𝑅 Se 𝐴
64, 5wa 399 . . 3 wff (𝑅 We 𝐴𝑅 Se 𝐴)
7 vh . . . . . 6 setvar
8 cvv 3399 . . . . . 6 class V
9 vu . . . . . . . . . . 11 setvar 𝑢
109cv 1541 . . . . . . . . . 10 class 𝑢
11 vv . . . . . . . . . . 11 setvar 𝑣
1211cv 1541 . . . . . . . . . 10 class 𝑣
1310, 12, 2wbr 5031 . . . . . . . . 9 wff 𝑢𝑅𝑣
1413wn 3 . . . . . . . 8 wff ¬ 𝑢𝑅𝑣
15 vj . . . . . . . . . . . 12 setvar 𝑗
1615cv 1541 . . . . . . . . . . 11 class 𝑗
17 vw . . . . . . . . . . . 12 setvar 𝑤
1817cv 1541 . . . . . . . . . . 11 class 𝑤
1916, 18, 2wbr 5031 . . . . . . . . . 10 wff 𝑗𝑅𝑤
207cv 1541 . . . . . . . . . . 11 class
2120crn 5527 . . . . . . . . . 10 class ran
2219, 15, 21wral 3054 . . . . . . . . 9 wff 𝑗 ∈ ran 𝑗𝑅𝑤
2322, 17, 1crab 3058 . . . . . . . 8 class {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
2414, 9, 23wral 3054 . . . . . . 7 wff 𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣
2524, 11, 23crio 7129 . . . . . 6 class (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
267, 8, 25cmpt 5111 . . . . 5 class ( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
2726crecs 8039 . . . 4 class recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
28 vz . . . . . . . . 9 setvar 𝑧
2928cv 1541 . . . . . . . 8 class 𝑧
30 vt . . . . . . . . 9 setvar 𝑡
3130cv 1541 . . . . . . . 8 class 𝑡
3229, 31, 2wbr 5031 . . . . . . 7 wff 𝑧𝑅𝑡
33 vx . . . . . . . . 9 setvar 𝑥
3433cv 1541 . . . . . . . 8 class 𝑥
3527, 34cima 5529 . . . . . . 7 class (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)
3632, 28, 35wral 3054 . . . . . 6 wff 𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
3736, 30, 1wrex 3055 . . . . 5 wff 𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
38 con0 6173 . . . . 5 class On
3937, 33, 38crab 3058 . . . 4 class {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}
4027, 39cres 5528 . . 3 class (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡})
41 c0 4212 . . 3 class
426, 40, 41cif 4415 . 2 class if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
433, 42wceq 1542 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  9051  oieq1  9052  oieq2  9053  nfoi  9054  oi0  9068
  Copyright terms: Public domain W3C validator