This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rankf

Description: The domain and codomain 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 eqabcb ⊢ ( { 𝑥 ∣ ∃ 𝑧 𝑧 = ∩ { 𝑦 ∈ 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