Theorem rankr1clem

Description: Lemma for rankr1c . (Contributed by NM, 6-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	rankr1clem	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐵 ⊆ ( rank ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rankr1ag	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
2	1	notbid	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
3		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
4	3	simpri	⊢ Lim dom 𝑅1
5		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
6	4 5	ax-mp	⊢ Ord dom 𝑅1
7		ordelon	⊢ ( ( Ord dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
8	6 7	mpan	⊢ ( 𝐵 ∈ dom 𝑅1 → 𝐵 ∈ On )
9	8	adantl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
10		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
11		ontri1	⊢ ( ( 𝐵 ∈ On ∧ ( rank ‘ 𝐴 ) ∈ On ) → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
12	9 10 11	sylancl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
13	2 12	bitr4d	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐵 ⊆ ( rank ‘ 𝐴 ) ) )