Detailed syntax breakdown of Definition df-oi
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class 𝐴 |
2 | | cR |
. . 3
class 𝑅 |
3 | 1, 2 | coi 9049 |
. 2
class
OrdIso(𝑅, 𝐴) |
4 | 1, 2 | wwe 5483 |
. . . 4
wff 𝑅 We 𝐴 |
5 | 1, 2 | wse 5482 |
. . . 4
wff 𝑅 Se 𝐴 |
6 | 4, 5 | wa 399 |
. . 3
wff (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) |
7 | | vh |
. . . . . 6
setvar ℎ |
8 | | cvv 3399 |
. . . . . 6
class
V |
9 | | vu |
. . . . . . . . . . 11
setvar 𝑢 |
10 | 9 | cv 1541 |
. . . . . . . . . 10
class 𝑢 |
11 | | vv |
. . . . . . . . . . 11
setvar 𝑣 |
12 | 11 | cv 1541 |
. . . . . . . . . 10
class 𝑣 |
13 | 10, 12, 2 | wbr 5031 |
. . . . . . . . 9
wff 𝑢𝑅𝑣 |
14 | 13 | wn 3 |
. . . . . . . 8
wff ¬
𝑢𝑅𝑣 |
15 | | vj |
. . . . . . . . . . . 12
setvar 𝑗 |
16 | 15 | cv 1541 |
. . . . . . . . . . 11
class 𝑗 |
17 | | vw |
. . . . . . . . . . . 12
setvar 𝑤 |
18 | 17 | cv 1541 |
. . . . . . . . . . 11
class 𝑤 |
19 | 16, 18, 2 | wbr 5031 |
. . . . . . . . . 10
wff 𝑗𝑅𝑤 |
20 | 7 | cv 1541 |
. . . . . . . . . . 11
class ℎ |
21 | 20 | crn 5527 |
. . . . . . . . . 10
class ran ℎ |
22 | 19, 15, 21 | wral 3054 |
. . . . . . . . 9
wff
∀𝑗 ∈ ran
ℎ 𝑗𝑅𝑤 |
23 | 22, 17, 1 | crab 3058 |
. . . . . . . 8
class {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} |
24 | 14, 9, 23 | wral 3054 |
. . . . . . 7
wff
∀𝑢 ∈
{𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 |
25 | 24, 11, 23 | crio 7129 |
. . . . . 6
class
(℩𝑣
∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) |
26 | 7, 8, 25 | cmpt 5111 |
. . . . 5
class (ℎ ∈ V ↦
(℩𝑣 ∈
{𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
27 | 26 | crecs 8039 |
. . . 4
class
recs((ℎ ∈ V
↦ (℩𝑣
∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) |
28 | | vz |
. . . . . . . . 9
setvar 𝑧 |
29 | 28 | cv 1541 |
. . . . . . . 8
class 𝑧 |
30 | | vt |
. . . . . . . . 9
setvar 𝑡 |
31 | 30 | cv 1541 |
. . . . . . . 8
class 𝑡 |
32 | 29, 31, 2 | wbr 5031 |
. . . . . . 7
wff 𝑧𝑅𝑡 |
33 | | vx |
. . . . . . . . 9
setvar 𝑥 |
34 | 33 | cv 1541 |
. . . . . . . 8
class 𝑥 |
35 | 27, 34 | cima 5529 |
. . . . . . 7
class
(recs((ℎ ∈ V
↦ (℩𝑣
∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥) |
36 | 32, 28, 35 | wral 3054 |
. . . . . 6
wff
∀𝑧 ∈
(recs((ℎ ∈ V ↦
(℩𝑣 ∈
{𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡 |
37 | 36, 30, 1 | wrex 3055 |
. . . . 5
wff
∃𝑡 ∈
𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦
(℩𝑣 ∈
{𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡 |
38 | | con0 6173 |
. . . . 5
class
On |
39 | 37, 33, 38 | crab 3058 |
. . . 4
class {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡} |
40 | 27, 39 | cres 5528 |
. . 3
class
(recs((ℎ ∈ V
↦ (℩𝑣
∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}) |
41 | | c0 4212 |
. . 3
class
∅ |
42 | 6, 40, 41 | cif 4415 |
. 2
class if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅) |
43 | 3, 42 | wceq 1542 |
1
wff
OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅) |