Metamath Proof Explorer

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 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
3 2 simpri ⊢ Lim dom 𝑅1
4 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
5 3 4 ax-mp ⊢ Ord dom 𝑅1
6 ordelord ⊢ ( ( Ord dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → Ord 𝐵 )
7 5 6 mpan ⊢ ( 𝐵 ∈ dom 𝑅1 → Ord 𝐵 )
8 7 adantl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → Ord 𝐵 )
9 ordsucss ⊢ ( Ord 𝐵 → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → suc ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
10 8 9 syl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → suc ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
11 rankidb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
12 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
13 11 12 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
14 r1ord3g ⊢ ( ( suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( suc ( rank ‘ 𝐴 ) ⊆ 𝐵 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
15 13 14 sylan ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( suc ( rank ‘ 𝐴 ) ⊆ 𝐵 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
16 11 adantr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
17 ssel ⊢ ( ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
18 16 17 syl5com ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
19 10 15 18 3syld ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
20 1 19 impbid2 ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )