Metamath Proof Explorer


Theorem rankf

Description: The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 12-Sep-2013)

Ref Expression
Assertion rankf rank : ( 𝑅1 “ On ) ⟶ On

Proof

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