Theorem ranksnb

Description: The rank of a singleton. Theorem 15.17(v) of Monk1 p. 112. (Contributed by Mario Carneiro, 10-Jun-2013)

	Ref	Expression
Assertion	ranksnb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑦 = 𝐴 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐴 ) )
2	1	eleq1d	⊢ ( 𝑦 = 𝐴 → ( ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ( rank ‘ 𝐴 ) ∈ 𝑥 ) )
3	2	ralsng	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ( rank ‘ 𝐴 ) ∈ 𝑥 ) )
4	3	rabbidv	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } = { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
5	4	inteqd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } = ∩ { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
6		snwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
7		rankval3b	⊢ ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } )
8	6 7	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } )
9		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
10		onsucmin	⊢ ( ( rank ‘ 𝐴 ) ∈ On → suc ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
11	9 10	mp1i	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
12	5 8 11	3eqtr4d	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )