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

Definition df-oi 8568
 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 8567 . 2 class OrdIso(𝑅, 𝐴)
41, 2wwe 5212 . . . 4 wff 𝑅 We 𝐴
51, 2wse 5211 . . . 4 wff 𝑅 Se 𝐴
64, 5wa 383 . . 3 wff (𝑅 We 𝐴𝑅 Se 𝐴)
7 vh . . . . . 6 setvar
8 cvv 3328 . . . . . 6 class V
9 vu . . . . . . . . . . 11 setvar 𝑢
109cv 1619 . . . . . . . . . 10 class 𝑢
11 vv . . . . . . . . . . 11 setvar 𝑣
1211cv 1619 . . . . . . . . . 10 class 𝑣
1310, 12, 2wbr 4792 . . . . . . . . 9 wff 𝑢𝑅𝑣
1413wn 3 . . . . . . . 8 wff ¬ 𝑢𝑅𝑣
15 vj . . . . . . . . . . . 12 setvar 𝑗
1615cv 1619 . . . . . . . . . . 11 class 𝑗
17 vw . . . . . . . . . . . 12 setvar 𝑤
1817cv 1619 . . . . . . . . . . 11 class 𝑤
1916, 18, 2wbr 4792 . . . . . . . . . 10 wff 𝑗𝑅𝑤
207cv 1619 . . . . . . . . . . 11 class
2120crn 5255 . . . . . . . . . 10 class ran
2219, 15, 21wral 3038 . . . . . . . . 9 wff 𝑗 ∈ ran 𝑗𝑅𝑤
2322, 17, 1crab 3042 . . . . . . . 8 class {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
2414, 9, 23wral 3038 . . . . . . 7 wff 𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣
2524, 11, 23crio 6761 . . . . . 6 class (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
267, 8, 25cmpt 4869 . . . . 5 class ( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
2726crecs 7624 . . . 4 class recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
28 vz . . . . . . . . 9 setvar 𝑧
2928cv 1619 . . . . . . . 8 class 𝑧
30 vt . . . . . . . . 9 setvar 𝑡
3130cv 1619 . . . . . . . 8 class 𝑡
3229, 31, 2wbr 4792 . . . . . . 7 wff 𝑧𝑅𝑡
33 vx . . . . . . . . 9 setvar 𝑥
3433cv 1619 . . . . . . . 8 class 𝑥
3527, 34cima 5257 . . . . . . 7 class (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)
3632, 28, 35wral 3038 . . . . . 6 wff 𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
3736, 30, 1wrex 3039 . . . . 5 wff 𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
38 con0 5872 . . . . 5 class On
3937, 33, 38crab 3042 . . . 4 class {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}
4027, 39cres 5256 . . 3 class (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡})
41 c0 4046 . . 3 class
426, 40, 41cif 4218 . 2 class if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
433, 42wceq 1620 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  8569  oieq1  8570  oieq2  8571  nfoi  8572  oi0  8586
 Copyright terms: Public domain W3C validator