Theorem r1ord3g

Description: Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of BellMachover p. 478. (Contributed by NM, 22-Sep-2003)

	Ref	Expression
Assertion	r1ord3g	|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A C_ B -> ( R1 ` A ) C_ ( R1 ` B ) ) )

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	4	sseli	|- ( A e. dom R1 -> A e. On )
6	4	sseli	|- ( B e. dom R1 -> B e. On )
7		onsseleq	|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
8	5 6 7	syl2an	|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
9		r1tr	|- Tr ( R1 ` B )
10		r1ordg	|- ( B e. dom R1 -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )
11	10	adantl	|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )
12		trss	|- ( Tr ( R1 ` B ) -> ( ( R1 ` A ) e. ( R1 ` B ) -> ( R1 ` A ) C_ ( R1 ` B ) ) )
13	9 11 12	mpsylsyld	|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A e. B -> ( R1 ` A ) C_ ( R1 ` B ) ) )
14		fveq2	|- ( A = B -> ( R1 ` A ) = ( R1 ` B ) )
15		eqimss	|- ( ( R1 ` A ) = ( R1 ` B ) -> ( R1 ` A ) C_ ( R1 ` B ) )
16	14 15	syl	|- ( A = B -> ( R1 ` A ) C_ ( R1 ` B ) )
17	16	a1i	|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A = B -> ( R1 ` A ) C_ ( R1 ` B ) ) )
18	13 17	jaod	|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( ( A e. B \/ A = B ) -> ( R1 ` A ) C_ ( R1 ` B ) ) )
19	8 18	sylbid	|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A C_ B -> ( R1 ` A ) C_ ( R1 ` B ) ) )