Step |
Hyp |
Ref |
Expression |
1 |
|
df-rank |
⊢ rank = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ) |
2 |
1
|
funmpt2 |
⊢ Fun rank |
3 |
|
mptv |
⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ) = { 〈 𝑥 , 𝑧 〉 ∣ 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } |
4 |
1 3
|
eqtri |
⊢ rank = { 〈 𝑥 , 𝑧 〉 ∣ 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } |
5 |
4
|
dmeqi |
⊢ dom rank = dom { 〈 𝑥 , 𝑧 〉 ∣ 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } |
6 |
|
dmopab |
⊢ dom { 〈 𝑥 , 𝑧 〉 ∣ 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } = { 𝑥 ∣ ∃ 𝑧 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } |
7 |
|
abeq1 |
⊢ ( { 𝑥 ∣ ∃ 𝑧 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } = ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑥 ( ∃ 𝑧 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ↔ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) ) |
8 |
|
rankwflemb |
⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) ) |
9 |
|
intexrab |
⊢ ( ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) ↔ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ V ) |
10 |
|
isset |
⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ V ↔ ∃ 𝑧 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ) |
11 |
8 9 10
|
3bitrri |
⊢ ( ∃ 𝑧 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ↔ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) |
12 |
7 11
|
mpgbir |
⊢ { 𝑥 ∣ ∃ 𝑧 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } = ∪ ( 𝑅1 “ On ) |
13 |
6 12
|
eqtri |
⊢ dom { 〈 𝑥 , 𝑧 〉 ∣ 𝑧 = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } } = ∪ ( 𝑅1 “ On ) |
14 |
5 13
|
eqtri |
⊢ dom rank = ∪ ( 𝑅1 “ On ) |
15 |
|
df-fn |
⊢ ( rank Fn ∪ ( 𝑅1 “ On ) ↔ ( Fun rank ∧ dom rank = ∪ ( 𝑅1 “ On ) ) ) |
16 |
2 14 15
|
mpbir2an |
⊢ rank Fn ∪ ( 𝑅1 “ On ) |
17 |
|
rabn0 |
⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ ↔ ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) ) |
18 |
8 17
|
bitr4i |
⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ ) |
19 |
|
intex |
⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ ↔ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ V ) |
20 |
|
vex |
⊢ 𝑥 ∈ V |
21 |
1
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ V ∧ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ V ) → ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ) |
22 |
20 21
|
mpan |
⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ V → ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ) |
23 |
19 22
|
sylbi |
⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ → ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ) |
24 |
|
ssrab2 |
⊢ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ⊆ On |
25 |
|
oninton |
⊢ ( ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ⊆ On ∧ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ ) → ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ On ) |
26 |
24 25
|
mpan |
⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ → ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ On ) |
27 |
23 26
|
eqeltrd |
⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ → ( rank ‘ 𝑥 ) ∈ On ) |
28 |
18 27
|
sylbi |
⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝑥 ) ∈ On ) |
29 |
28
|
rgen |
⊢ ∀ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ( rank ‘ 𝑥 ) ∈ On |
30 |
|
ffnfv |
⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On ↔ ( rank Fn ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ( rank ‘ 𝑥 ) ∈ On ) ) |
31 |
16 29 30
|
mpbir2an |
⊢ rank : ∪ ( 𝑅1 “ On ) ⟶ On |