Metamath Proof Explorer

Theorem isf32lem3

Description: Lemma for isfin3-2 . Being a chain, difference sets are disjoint (one case). (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a 
|- ( ph -> F : _om --> ~P G )
isf32lem.b 
|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
isf32lem.c 
|- ( ph -> -. |^| ran F e. ran F )
Assertion isf32lem3 
|- ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )

Proof

Step Hyp Ref Expression
1 isf32lem.a 
 |-  ( ph -> F : _om --> ~P G )
2 isf32lem.b 
 |-  ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
3 isf32lem.c 
 |-  ( ph -> -. |^| ran F e. ran F )
4 eldifi 
 |-  ( a e. ( ( F ` A ) \ ( F ` suc A ) ) -> a e. ( F ` A ) )
5 simpll 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> A e. _om )
6 peano2 
 |-  ( B e. _om -> suc B e. _om )
7 6 ad2antlr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> suc B e. _om )
8 nnord 
 |-  ( A e. _om -> Ord A )
9 8 ad2antrr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> Ord A )
10 simprl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> B e. A )
11 ordsucss 
 |-  ( Ord A -> ( B e. A -> suc B C_ A ) )
12 9 10 11 sylc 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> suc B C_ A )
13 simprr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> ph )
14 1 2 3 isf32lem1 
 |-  ( ( ( A e. _om /\ suc B e. _om ) /\ ( suc B C_ A /\ ph ) ) -> ( F ` A ) C_ ( F ` suc B ) )
15 5 7 12 13 14 syl22anc 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> ( F ` A ) C_ ( F ` suc B ) )
16 15 sseld 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> ( a e. ( F ` A ) -> a e. ( F ` suc B ) ) )
17 elndif 
 |-  ( a e. ( F ` suc B ) -> -. a e. ( ( F ` B ) \ ( F ` suc B ) ) )
18 4 16 17 syl56 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> ( a e. ( ( F ` A ) \ ( F ` suc A ) ) -> -. a e. ( ( F ` B ) \ ( F ` suc B ) ) ) )
19 18 ralrimiv 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> A. a e. ( ( F ` A ) \ ( F ` suc A ) ) -. a e. ( ( F ` B ) \ ( F ` suc B ) ) )
20 disj 
 |-  ( ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) <-> A. a e. ( ( F ` A ) \ ( F ` suc A ) ) -. a e. ( ( F ` B ) \ ( F ` suc B ) ) )
21 19 20 sylibr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )