Metamath Proof Explorer

Theorem isf32lem4

Description: Lemma for isfin3-2 . Being a chain, difference sets are disjoint. (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 isf32lem4 
|- ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( 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 simplrr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ A e. B ) -> B e. _om )
5 simplrl 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ A e. B ) -> A e. _om )
6 simpr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ A e. B ) -> A e. B )
7 simplll 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ A e. B ) -> ph )
8 incom 
 |-  ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = ( ( ( F ` B ) \ ( F ` suc B ) ) i^i ( ( F ` A ) \ ( F ` suc A ) ) )
9 1 2 3 isf32lem3 
 |-  ( ( ( B e. _om /\ A e. _om ) /\ ( A e. B /\ ph ) ) -> ( ( ( F ` B ) \ ( F ` suc B ) ) i^i ( ( F ` A ) \ ( F ` suc A ) ) ) = (/) )
10 8 9 syl5eq 
 |-  ( ( ( B e. _om /\ A e. _om ) /\ ( A e. B /\ ph ) ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )
11 4 5 6 7 10 syl22anc 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ A e. B ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )
12 simplrl 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ B e. A ) -> A e. _om )
13 simplrr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ B e. A ) -> B e. _om )
14 simpr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ B e. A ) -> B e. A )
15 simplll 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ B e. A ) -> ph )
16 1 2 3 isf32lem3 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B e. A /\ ph ) ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )
17 12 13 14 15 16 syl22anc 
 |-  ( ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) /\ B e. A ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )
18 simplr 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> A =/= B )
19 nnord 
 |-  ( A e. _om -> Ord A )
20 nnord 
 |-  ( B e. _om -> Ord B )
21 ordtri3 
 |-  ( ( Ord A /\ Ord B ) -> ( A = B <-> -. ( A e. B \/ B e. A ) ) )
22 19 20 21 syl2an 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A = B <-> -. ( A e. B \/ B e. A ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( A = B <-> -. ( A e. B \/ B e. A ) ) )
24 23 necon2abid 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( A e. B \/ B e. A ) <-> A =/= B ) )
25 18 24 mpbird 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B \/ B e. A ) )
26 11 17 25 mpjaodan 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )