Theorem rankr1ag

Description: A version of rankr1a that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		rankr1ai	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
2		r1dmlim	⊢ Lim dom 𝑅1
3		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
4	2 3	ax-mp	⊢ Ord dom 𝑅1
5		ordelord	⊢ ( ( Ord dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → Ord 𝐵 )
6	4 5	mpan	⊢ ( 𝐵 ∈ dom 𝑅1 → Ord 𝐵 )
7	6	adantl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → Ord 𝐵 )
8		ordsucss	⊢ ( Ord 𝐵 → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → suc ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
9	7 8	syl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → suc ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
10		rankidb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
11		elfvdm	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
12	10 11	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
13		r1ord3g	⊢ ( ( suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( suc ( rank ‘ 𝐴 ) ⊆ 𝐵 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
14	12 13	sylan	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( suc ( rank ‘ 𝐴 ) ⊆ 𝐵 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
15	10	adantr	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
16		ssel	⊢ ( ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
17	15 16	syl5com	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
18	9 14 17	3syld	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
19	1 18	impbid2	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )