Metamath Proof Explorer

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