Theorem r1elwf

Description: Any element of (any stage of) the cumulative hierarchy of sets is well-founded (recall that U. ( R1 " On ) is the class of well-founded sets). (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	r1elwf	|- ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	|- Lim dom R1
2		limord	|- ( Lim dom R1 -> Ord dom R1 )
3		ordsson	|- ( Ord dom R1 -> dom R1 C_ On )
4	1 2 3	mp2b	|- dom R1 C_ On
5		elfvdm	|- ( A e. ( R1 ` B ) -> B e. dom R1 )
6	4 5	sselid	|- ( A e. ( R1 ` B ) -> B e. On )
7		r1tr	|- Tr ( R1 ` B )
8		trss	|- ( Tr ( R1 ` B ) -> ( A e. ( R1 ` B ) -> A C_ ( R1 ` B ) ) )
9	7 8	ax-mp	|- ( A e. ( R1 ` B ) -> A C_ ( R1 ` B ) )
10		elpwg	|- ( A e. ( R1 ` B ) -> ( A e. ~P ( R1 ` B ) <-> A C_ ( R1 ` B ) ) )
11	9 10	mpbird	|- ( A e. ( R1 ` B ) -> A e. ~P ( R1 ` B ) )
12		r1sucg	|- ( B e. dom R1 -> ( R1 ` suc B ) = ~P ( R1 ` B ) )
13	5 12	syl	|- ( A e. ( R1 ` B ) -> ( R1 ` suc B ) = ~P ( R1 ` B ) )
14	11 13	eleqtrrd	|- ( A e. ( R1 ` B ) -> A e. ( R1 ` suc B ) )
15		suceq	|- ( x = B -> suc x = suc B )
16	15	fveq2d	|- ( x = B -> ( R1 ` suc x ) = ( R1 ` suc B ) )
17	16	eleq2d	|- ( x = B -> ( A e. ( R1 ` suc x ) <-> A e. ( R1 ` suc B ) ) )
18	17	rspcev	|- ( ( B e. On /\ A e. ( R1 ` suc B ) ) -> E. x e. On A e. ( R1 ` suc x ) )
19	6 14 18	syl2anc	|- ( A e. ( R1 ` B ) -> E. x e. On A e. ( R1 ` suc x ) )
20		rankwflemb	|- ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )
21	19 20	sylibr	|- ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )