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	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		rankr1ai	|- ( A e. ( R1 ` B ) -> ( rank ` A ) e. B )
2		r1dmlim	|- Lim dom R1
3		limord	|- ( Lim dom R1 -> Ord dom R1 )
4	2 3	ax-mp	|- Ord dom R1
5		ordelord	|- ( ( Ord dom R1 /\ B e. dom R1 ) -> Ord B )
6	4 5	mpan	|- ( B e. dom R1 -> Ord B )
7	6	adantl	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> Ord B )
8		ordsucss	|- ( Ord B -> ( ( rank ` A ) e. B -> suc ( rank ` A ) C_ B ) )
9	7 8	syl	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( rank ` A ) e. B -> suc ( rank ` A ) C_ B ) )
10		rankidb	|- ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )
11		elfvdm	|- ( A e. ( R1 ` suc ( rank ` A ) ) -> suc ( rank ` A ) e. dom R1 )
12	10 11	syl	|- ( A e. U. ( R1 " On ) -> suc ( rank ` A ) e. dom R1 )
13		r1ord3g	|- ( ( suc ( rank ` A ) e. dom R1 /\ B e. dom R1 ) -> ( suc ( rank ` A ) C_ B -> ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) ) )
14	12 13	sylan	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( suc ( rank ` A ) C_ B -> ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) ) )
15	10	adantr	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> A e. ( R1 ` suc ( rank ` A ) ) )
16		ssel	|- ( ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) -> ( A e. ( R1 ` suc ( rank ` A ) ) -> A e. ( R1 ` B ) ) )
17	15 16	syl5com	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) -> A e. ( R1 ` B ) ) )
18	9 14 17	3syld	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( rank ` A ) e. B -> A e. ( R1 ` B ) ) )
19	1 18	impbid2	|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )