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