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		r1dmlim	⊢ Lim dom 𝑅1
4		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
5	3 4	ax-mp	⊢ Ord dom 𝑅1
6		ordelon	⊢ ( ( Ord dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
7	5 6	mpan	⊢ ( 𝐵 ∈ dom 𝑅1 → 𝐵 ∈ On )
8	7	adantl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
9		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
10		ontri1	⊢ ( ( 𝐵 ∈ On ∧ ( rank ‘ 𝐴 ) ∈ On ) → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
11	8 9 10	sylancl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
12	2 11	bitr4d	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐵 ⊆ ( rank ‘ 𝐴 ) ) )