Definition df-oi 9550

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	coi 9549	. 2 class OrdIso(𝑅, 𝐴)
4	1, 2	wwe 5636	. . . 4 wff 𝑅 We 𝐴
5	1, 2	wse 5635	. . . 4 wff 𝑅 Se 𝐴
6	4, 5	wa 395	. . 3 wff (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴)
7		vh	. . . . . 6 setvar ℎ
8		cvv 3480	. . . . . 6 class V
9		vu	. . . . . . . . . . 11 setvar 𝑢
10	9	cv 1539	. . . . . . . . . 10 class 𝑢
11		vv	. . . . . . . . . . 11 setvar 𝑣
12	11	cv 1539	. . . . . . . . . 10 class 𝑣
13	10, 12, 2	wbr 5143	. . . . . . . . 9 wff 𝑢𝑅𝑣
14	13	wn 3	. . . . . . . 8 wff ¬ 𝑢𝑅𝑣
15		vj	. . . . . . . . . . . 12 setvar 𝑗
16	15	cv 1539	. . . . . . . . . . 11 class 𝑗
17		vw	. . . . . . . . . . . 12 setvar 𝑤
18	17	cv 1539	. . . . . . . . . . 11 class 𝑤
19	16, 18, 2	wbr 5143	. . . . . . . . . 10 wff 𝑗𝑅𝑤
20	7	cv 1539	. . . . . . . . . . 11 class ℎ
21	20	crn 5686	. . . . . . . . . 10 class ran ℎ
22	19, 15, 21	wral 3061	. . . . . . . . 9 wff ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤
23	22, 17, 1	crab 3436	. . . . . . . 8 class {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}
24	14, 9, 23	wral 3061	. . . . . . 7 wff ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣
25	24, 11, 23	crio 7387	. . . . . 6 class (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
26	7, 8, 25	cmpt 5225	. . . . 5 class (ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
27	26	crecs 8410	. . . 4 class recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
28		vz	. . . . . . . . 9 setvar 𝑧
29	28	cv 1539	. . . . . . . 8 class 𝑧
30		vt	. . . . . . . . 9 setvar 𝑡
31	30	cv 1539	. . . . . . . 8 class 𝑡
32	29, 31, 2	wbr 5143	. . . . . . 7 wff 𝑧𝑅𝑡
33		vx	. . . . . . . . 9 setvar 𝑥
34	33	cv 1539	. . . . . . . 8 class 𝑥
35	27, 34	cima 5688	. . . . . . 7 class (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)
36	32, 28, 35	wral 3061	. . . . . 6 wff ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
37	36, 30, 1	wrex 3070	. . . . 5 wff ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡
38		con0 6384	. . . . 5 class On
39	37, 33, 38	crab 3436	. . . 4 class {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}
40	27, 39	cres 5687	. . 3 class (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡})
41		c0 4333	. . 3 class ∅
42	6, 40, 41	cif 4525	. 2 class if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
43	3, 42	wceq 1540	1 wff OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)

This definition is referenced by:  dfoi  9551  oieq1  9552  oieq2  9553  nfoi  9554  oi0  9568