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 ( 𝑅 , 𝐴 ) = if ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 𝑅
1 cA 𝐴
2 1 0 coi OrdIso ( 𝑅 , 𝐴 )
3 1 0 wwe 𝑅 We 𝐴
4 1 0 wse 𝑅 Se 𝐴
5 3 4 wa ( 𝑅 We 𝐴𝑅 Se 𝐴 )
6 vh
7 cvv V
8 vv 𝑣
9 vw 𝑤
10 vj 𝑗
11 6 cv
12 11 crn ran
13 10 cv 𝑗
14 9 cv 𝑤
15 13 14 0 wbr 𝑗 𝑅 𝑤
16 15 10 12 wral 𝑗 ∈ ran 𝑗 𝑅 𝑤
17 16 9 1 crab { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 }
18 vu 𝑢
19 18 cv 𝑢
20 8 cv 𝑣
21 19 20 0 wbr 𝑢 𝑅 𝑣
22 21 wn ¬ 𝑢 𝑅 𝑣
23 22 18 17 wral 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣
24 23 8 17 crio ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 )
25 6 7 24 cmpt ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) )
26 25 crecs recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) )
27 vx 𝑥
28 con0 On
29 vt 𝑡
30 vz 𝑧
31 27 cv 𝑥
32 26 31 cima ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 )
33 30 cv 𝑧
34 29 cv 𝑡
35 33 34 0 wbr 𝑧 𝑅 𝑡
36 35 30 32 wral 𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡
37 36 29 1 wrex 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡
38 37 27 28 crab { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 }
39 26 38 cres ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } )
40 c0
41 5 39 40 cif if ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ )
42 2 41 wceq OrdIso ( 𝑅 , 𝐴 ) = if ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) , ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) ↾ { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } ) , ∅ )