Step | Hyp | Ref
| Expression |
1 | | df-oi 9059 |
. 2
⊢
OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}), ∅) |
2 | | nfoi.1 |
. . . . 5
⊢
Ⅎ𝑥𝑅 |
3 | | nfoi.2 |
. . . . 5
⊢
Ⅎ𝑥𝐴 |
4 | 2, 3 | nfwe 5511 |
. . . 4
⊢
Ⅎ𝑥 𝑅 We 𝐴 |
5 | 2, 3 | nfse 5510 |
. . . 4
⊢
Ⅎ𝑥 𝑅 Se 𝐴 |
6 | 4, 5 | nfan 1906 |
. . 3
⊢
Ⅎ𝑥(𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) |
7 | | nfcv 2900 |
. . . . . 6
⊢
Ⅎ𝑥V |
8 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑥ran
ℎ |
9 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑗 |
10 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑤 |
11 | 9, 2, 10 | nfbr 5087 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑗𝑅𝑤 |
12 | 8, 11 | nfralw 3139 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤 |
13 | 12, 3 | nfrabw 3289 |
. . . . . . . 8
⊢
Ⅎ𝑥{𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} |
14 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑢 |
15 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑣 |
16 | 14, 2, 15 | nfbr 5087 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑢𝑅𝑣 |
17 | 16 | nfn 1864 |
. . . . . . . 8
⊢
Ⅎ𝑥 ¬ 𝑢𝑅𝑣 |
18 | 13, 17 | nfralw 3139 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 |
19 | 18, 13 | nfriota 7152 |
. . . . . 6
⊢
Ⅎ𝑥(℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) |
20 | 7, 19 | nfmpt 5137 |
. . . . 5
⊢
Ⅎ𝑥(ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) |
21 | 20 | nfrecs 8052 |
. . . 4
⊢
Ⅎ𝑥recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) |
22 | | nfcv 2900 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑎 |
23 | 21, 22 | nfima 5921 |
. . . . . . 7
⊢
Ⅎ𝑥(recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎) |
24 | | nfcv 2900 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑧 |
25 | | nfcv 2900 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑡 |
26 | 24, 2, 25 | nfbr 5087 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑧𝑅𝑡 |
27 | 23, 26 | nfralw 3139 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡 |
28 | 3, 27 | nfrex 3220 |
. . . . 5
⊢
Ⅎ𝑥∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡 |
29 | | nfcv 2900 |
. . . . 5
⊢
Ⅎ𝑥On |
30 | 28, 29 | nfrabw 3289 |
. . . 4
⊢
Ⅎ𝑥{𝑎 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡} |
31 | 21, 30 | nfres 5837 |
. . 3
⊢
Ⅎ𝑥(recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}) |
32 | | nfcv 2900 |
. . 3
⊢
Ⅎ𝑥∅ |
33 | 6, 31, 32 | nfif 4454 |
. 2
⊢
Ⅎ𝑥if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}), ∅) |
34 | 1, 33 | nfcxfr 2898 |
1
⊢
Ⅎ𝑥OrdIso(𝑅, 𝐴) |