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