Metamath Proof Explorer

Theorem oacomf1olem

Description: Lemma for oacomf1o . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypothesis oacomf1olem.1 
|- F = ( x e. A |-> ( B +o x ) )
Assertion oacomf1olem 
|- ( ( A e. On /\ B e. On ) -> ( F : A -1-1-onto-> ran F /\ ( ran F i^i B ) = (/) ) )

Proof

Step Hyp Ref Expression
1 oacomf1olem.1 
 |-  F = ( x e. A |-> ( B +o x ) )
2 oaf1o 
 |-  ( B e. On -> ( x e. On |-> ( B +o x ) ) : On -1-1-onto-> ( On \ B ) )
3 2 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( x e. On |-> ( B +o x ) ) : On -1-1-onto-> ( On \ B ) )
4 f1of1 
 |-  ( ( x e. On |-> ( B +o x ) ) : On -1-1-onto-> ( On \ B ) -> ( x e. On |-> ( B +o x ) ) : On -1-1-> ( On \ B ) )
5 3 4 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( x e. On |-> ( B +o x ) ) : On -1-1-> ( On \ B ) )
6 onss 
 |-  ( A e. On -> A C_ On )
7 6 adantr 
 |-  ( ( A e. On /\ B e. On ) -> A C_ On )
8 f1ssres 
 |-  ( ( ( x e. On |-> ( B +o x ) ) : On -1-1-> ( On \ B ) /\ A C_ On ) -> ( ( x e. On |-> ( B +o x ) ) |` A ) : A -1-1-> ( On \ B ) )
9 5 7 8 syl2anc 
 |-  ( ( A e. On /\ B e. On ) -> ( ( x e. On |-> ( B +o x ) ) |` A ) : A -1-1-> ( On \ B ) )
10 7 resmptd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( x e. On |-> ( B +o x ) ) |` A ) = ( x e. A |-> ( B +o x ) ) )
11 10 1 eqtr4di 
 |-  ( ( A e. On /\ B e. On ) -> ( ( x e. On |-> ( B +o x ) ) |` A ) = F )
12 f1eq1 
 |-  ( ( ( x e. On |-> ( B +o x ) ) |` A ) = F -> ( ( ( x e. On |-> ( B +o x ) ) |` A ) : A -1-1-> ( On \ B ) <-> F : A -1-1-> ( On \ B ) ) )
13 11 12 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( ( x e. On |-> ( B +o x ) ) |` A ) : A -1-1-> ( On \ B ) <-> F : A -1-1-> ( On \ B ) ) )
14 9 13 mpbid 
 |-  ( ( A e. On /\ B e. On ) -> F : A -1-1-> ( On \ B ) )
15 f1f1orn 
 |-  ( F : A -1-1-> ( On \ B ) -> F : A -1-1-onto-> ran F )
16 14 15 syl 
 |-  ( ( A e. On /\ B e. On ) -> F : A -1-1-onto-> ran F )
17 f1f 
 |-  ( F : A -1-1-> ( On \ B ) -> F : A --> ( On \ B ) )
18 frn 
 |-  ( F : A --> ( On \ B ) -> ran F C_ ( On \ B ) )
19 14 17 18 3syl 
 |-  ( ( A e. On /\ B e. On ) -> ran F C_ ( On \ B ) )
20 19 difss2d 
 |-  ( ( A e. On /\ B e. On ) -> ran F C_ On )
21 reldisj 
 |-  ( ran F C_ On -> ( ( ran F i^i B ) = (/) <-> ran F C_ ( On \ B ) ) )
22 20 21 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( ran F i^i B ) = (/) <-> ran F C_ ( On \ B ) ) )
23 19 22 mpbird 
 |-  ( ( A e. On /\ B e. On ) -> ( ran F i^i B ) = (/) )
24 16 23 jca 
 |-  ( ( A e. On /\ B e. On ) -> ( F : A -1-1-onto-> ran F /\ ( ran F i^i B ) = (/) ) )