Metamath Proof Explorer

Theorem addsuniflem

Description: Lemma for addsunif . State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsuniflem.1 
|- ( ph -> L <
addsuniflem.2 
|- ( ph -> M <
addsuniflem.3 
|- ( ph -> A = ( L |s R ) )
addsuniflem.4 
|- ( ph -> B = ( M |s S ) )
Assertion addsuniflem 
|- ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsuniflem.1 
 |-  ( ph -> L <
2 addsuniflem.2 
 |-  ( ph -> M <
3 addsuniflem.3 
 |-  ( ph -> A = ( L |s R ) )
4 addsuniflem.4 
 |-  ( ph -> B = ( M |s S ) )
5 1 cutscld 
 |-  ( ph -> ( L |s R ) e. No )
6 3 5 eqeltrd 
 |-  ( ph -> A e. No )
7 2 cutscld 
 |-  ( ph -> ( M |s S ) e. No )
8 4 7 eqeltrd 
 |-  ( ph -> B e. No )
9 addsval2 
 |-  ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) )
10 6 8 9 syl2anc 
 |-  ( ph -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) )
11 6 8 addcuts 
 |-  ( ph -> ( ( A +s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
12 11 simp2d 
 |-  ( ph -> ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
13 11 simp3d 
 |-  ( ph -> { ( A +s B ) } <
14 ovex 
 |-  ( A +s B ) e. _V
15 14 snnz 
 |-  { ( A +s B ) } =/= (/)
16 sltstr 
 |-  ( ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
17 15 16 mp3an3 
 |-  ( ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
18 12 13 17 syl2anc 
 |-  ( ph -> ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
19 1 3 cofcutr1d 
 |-  ( ph -> A. p e. ( _Left ` A ) E. l e. L p <_s l )
20 leftno 
 |-  ( p e. ( _Left ` A ) -> p e. No )
21 20 ad2antlr 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> p e. No )
22 sltsss1 
 |-  ( L < L C_ No )
23 1 22 syl 
 |-  ( ph -> L C_ No )
24 23 adantr 
 |-  ( ( ph /\ p e. ( _Left ` A ) ) -> L C_ No )
25 24 sselda 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> l e. No )
26 8 ad2antrr 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> B e. No )
27 21 25 26 leadds1d 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> ( p <_s l <-> ( p +s B ) <_s ( l +s B ) ) )
28 27 rexbidva 
 |-  ( ( ph /\ p e. ( _Left ` A ) ) -> ( E. l e. L p <_s l <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) )
29 28 ralbidva 
 |-  ( ph -> ( A. p e. ( _Left ` A ) E. l e. L p <_s l <-> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) ) )
30 19 29 mpbid 
 |-  ( ph -> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) )
31 eqeq1 
 |-  ( y = s -> ( y = ( l +s B ) <-> s = ( l +s B ) ) )
32 31 rexbidv 
 |-  ( y = s -> ( E. l e. L y = ( l +s B ) <-> E. l e. L s = ( l +s B ) ) )
33 32 rexab 
 |-  ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) )
34 rexcom4 
 |-  ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) )
35 ovex 
 |-  ( l +s B ) e. _V
36 breq2 
 |-  ( s = ( l +s B ) -> ( ( p +s B ) <_s s <-> ( p +s B ) <_s ( l +s B ) ) )
37 35 36 ceqsexv 
 |-  ( E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( p +s B ) <_s ( l +s B ) )
38 37 rexbii 
 |-  ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) )
39 r19.41v 
 |-  ( E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) )
40 39 exbii 
 |-  ( E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) )
41 34 38 40 3bitr3ri 
 |-  ( E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) )
42 33 41 bitri 
 |-  ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. l e. L ( p +s B ) <_s ( l +s B ) )
43 ssun1 
 |-  { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } )
44 ssrexv 
 |-  ( { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) )
45 43 44 ax-mp 
 |-  ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
46 42 45 sylbir 
 |-  ( E. l e. L ( p +s B ) <_s ( l +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
47 46 ralimi 
 |-  ( A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
48 30 47 syl 
 |-  ( ph -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
49 2 4 cofcutr1d 
 |-  ( ph -> A. q e. ( _Left ` B ) E. m e. M q <_s m )
50 leftno 
 |-  ( q e. ( _Left ` B ) -> q e. No )
51 50 ad2antlr 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> q e. No )
52 sltsss1 
 |-  ( M < M C_ No )
53 2 52 syl 
 |-  ( ph -> M C_ No )
54 53 adantr 
 |-  ( ( ph /\ q e. ( _Left ` B ) ) -> M C_ No )
55 54 sselda 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> m e. No )
56 6 ad2antrr 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> A e. No )
57 51 55 56 leadds2d 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> ( q <_s m <-> ( A +s q ) <_s ( A +s m ) ) )
58 57 rexbidva 
 |-  ( ( ph /\ q e. ( _Left ` B ) ) -> ( E. m e. M q <_s m <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) )
59 58 ralbidva 
 |-  ( ph -> ( A. q e. ( _Left ` B ) E. m e. M q <_s m <-> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) ) )
60 49 59 mpbid 
 |-  ( ph -> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) )
61 eqeq1 
 |-  ( z = s -> ( z = ( A +s m ) <-> s = ( A +s m ) ) )
62 61 rexbidv 
 |-  ( z = s -> ( E. m e. M z = ( A +s m ) <-> E. m e. M s = ( A +s m ) ) )
63 62 rexab 
 |-  ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) )
64 rexcom4 
 |-  ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) )
65 ovex 
 |-  ( A +s m ) e. _V
66 breq2 
 |-  ( s = ( A +s m ) -> ( ( A +s q ) <_s s <-> ( A +s q ) <_s ( A +s m ) ) )
67 65 66 ceqsexv 
 |-  ( E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( A +s q ) <_s ( A +s m ) )
68 67 rexbii 
 |-  ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) )
69 r19.41v 
 |-  ( E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) )
70 69 exbii 
 |-  ( E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) )
71 64 68 70 3bitr3ri 
 |-  ( E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) )
72 63 71 bitri 
 |-  ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. m e. M ( A +s q ) <_s ( A +s m ) )
73 ssun2 
 |-  { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } )
74 ssrexv 
 |-  ( { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
75 73 74 ax-mp 
 |-  ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
76 72 75 sylbir 
 |-  ( E. m e. M ( A +s q ) <_s ( A +s m ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
77 76 ralimi 
 |-  ( A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
78 60 77 syl 
 |-  ( ph -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
79 ralunb 
 |-  ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
80 eqeq1 
 |-  ( a = r -> ( a = ( p +s B ) <-> r = ( p +s B ) ) )
81 80 rexbidv 
 |-  ( a = r -> ( E. p e. ( _Left ` A ) a = ( p +s B ) <-> E. p e. ( _Left ` A ) r = ( p +s B ) ) )
82 81 ralab 
 |-  ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
83 ralcom4 
 |-  ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
84 ovex 
 |-  ( p +s B ) e. _V
85 breq1 
 |-  ( r = ( p +s B ) -> ( r <_s s <-> ( p +s B ) <_s s ) )
86 85 rexbidv 
 |-  ( r = ( p +s B ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) )
87 84 86 ceqsalv 
 |-  ( A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
88 87 ralbii 
 |-  ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
89 r19.23v 
 |-  ( A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
90 89 albii 
 |-  ( A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
91 83 88 90 3bitr3ri 
 |-  ( A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
92 82 91 bitri 
 |-  ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
93 eqeq1 
 |-  ( b = r -> ( b = ( A +s q ) <-> r = ( A +s q ) ) )
94 93 rexbidv 
 |-  ( b = r -> ( E. q e. ( _Left ` B ) b = ( A +s q ) <-> E. q e. ( _Left ` B ) r = ( A +s q ) ) )
95 94 ralab 
 |-  ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
96 ralcom4 
 |-  ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
97 ovex 
 |-  ( A +s q ) e. _V
98 breq1 
 |-  ( r = ( A +s q ) -> ( r <_s s <-> ( A +s q ) <_s s ) )
99 98 rexbidv 
 |-  ( r = ( A +s q ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
100 97 99 ceqsalv 
 |-  ( A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
101 100 ralbii 
 |-  ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
102 r19.23v 
 |-  ( A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
103 102 albii 
 |-  ( A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
104 96 101 103 3bitr3ri 
 |-  ( A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
105 95 104 bitri 
 |-  ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
106 92 105 anbi12i 
 |-  ( ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
107 79 106 bitri 
 |-  ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
108 48 78 107 sylanbrc 
 |-  ( ph -> A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s )
109 1 3 cofcutr2d 
 |-  ( ph -> A. e e. ( _Right ` A ) E. r e. R r <_s e )
110 sltsss2 
 |-  ( L < R C_ No )
111 1 110 syl 
 |-  ( ph -> R C_ No )
112 111 adantr 
 |-  ( ( ph /\ e e. ( _Right ` A ) ) -> R C_ No )
113 112 sselda 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> r e. No )
114 rightno 
 |-  ( e e. ( _Right ` A ) -> e e. No )
115 114 ad2antlr 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> e e. No )
116 8 ad2antrr 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> B e. No )
117 113 115 116 leadds1d 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> ( r <_s e <-> ( r +s B ) <_s ( e +s B ) ) )
118 117 rexbidva 
 |-  ( ( ph /\ e e. ( _Right ` A ) ) -> ( E. r e. R r <_s e <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) )
119 118 ralbidva 
 |-  ( ph -> ( A. e e. ( _Right ` A ) E. r e. R r <_s e <-> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) ) )
120 109 119 mpbid 
 |-  ( ph -> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) )
121 eqeq1 
 |-  ( w = b -> ( w = ( r +s B ) <-> b = ( r +s B ) ) )
122 121 rexbidv 
 |-  ( w = b -> ( E. r e. R w = ( r +s B ) <-> E. r e. R b = ( r +s B ) ) )
123 122 rexab 
 |-  ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) )
124 rexcom4 
 |-  ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) )
125 ovex 
 |-  ( r +s B ) e. _V
126 breq1 
 |-  ( b = ( r +s B ) -> ( b <_s ( e +s B ) <-> ( r +s B ) <_s ( e +s B ) ) )
127 125 126 ceqsexv 
 |-  ( E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( r +s B ) <_s ( e +s B ) )
128 127 rexbii 
 |-  ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) )
129 r19.41v 
 |-  ( E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) )
130 129 exbii 
 |-  ( E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) )
131 124 128 130 3bitr3ri 
 |-  ( E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) )
132 123 131 bitri 
 |-  ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) )
133 ssun1 
 |-  { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } )
134 ssrexv 
 |-  ( { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) )
135 133 134 ax-mp 
 |-  ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
136 132 135 sylbir 
 |-  ( E. r e. R ( r +s B ) <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
137 136 ralimi 
 |-  ( A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
138 120 137 syl 
 |-  ( ph -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
139 2 4 cofcutr2d 
 |-  ( ph -> A. f e. ( _Right ` B ) E. s e. S s <_s f )
140 sltsss2 
 |-  ( M < S C_ No )
141 2 140 syl 
 |-  ( ph -> S C_ No )
142 141 adantr 
 |-  ( ( ph /\ f e. ( _Right ` B ) ) -> S C_ No )
143 142 sselda 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> s e. No )
144 rightno 
 |-  ( f e. ( _Right ` B ) -> f e. No )
145 144 ad2antlr 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> f e. No )
146 6 ad2antrr 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> A e. No )
147 143 145 146 leadds2d 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> ( s <_s f <-> ( A +s s ) <_s ( A +s f ) ) )
148 147 rexbidva 
 |-  ( ( ph /\ f e. ( _Right ` B ) ) -> ( E. s e. S s <_s f <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) )
149 148 ralbidva 
 |-  ( ph -> ( A. f e. ( _Right ` B ) E. s e. S s <_s f <-> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) ) )
150 139 149 mpbid 
 |-  ( ph -> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) )
151 eqeq1 
 |-  ( t = b -> ( t = ( A +s s ) <-> b = ( A +s s ) ) )
152 151 rexbidv 
 |-  ( t = b -> ( E. s e. S t = ( A +s s ) <-> E. s e. S b = ( A +s s ) ) )
153 152 rexab 
 |-  ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) )
154 rexcom4 
 |-  ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) )
155 ovex 
 |-  ( A +s s ) e. _V
156 breq1 
 |-  ( b = ( A +s s ) -> ( b <_s ( A +s f ) <-> ( A +s s ) <_s ( A +s f ) ) )
157 155 156 ceqsexv 
 |-  ( E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( A +s s ) <_s ( A +s f ) )
158 157 rexbii 
 |-  ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) )
159 r19.41v 
 |-  ( E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) )
160 159 exbii 
 |-  ( E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) )
161 154 158 160 3bitr3ri 
 |-  ( E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) )
162 153 161 bitri 
 |-  ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) )
163 ssun2 
 |-  { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } )
164 ssrexv 
 |-  ( { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
165 163 164 ax-mp 
 |-  ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
166 162 165 sylbir 
 |-  ( E. s e. S ( A +s s ) <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
167 166 ralimi 
 |-  ( A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
168 150 167 syl 
 |-  ( ph -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
169 ralunb 
 |-  ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
170 eqeq1 
 |-  ( c = a -> ( c = ( e +s B ) <-> a = ( e +s B ) ) )
171 170 rexbidv 
 |-  ( c = a -> ( E. e e. ( _Right ` A ) c = ( e +s B ) <-> E. e e. ( _Right ` A ) a = ( e +s B ) ) )
172 171 ralab 
 |-  ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
173 ralcom4 
 |-  ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
174 ovex 
 |-  ( e +s B ) e. _V
175 breq2 
 |-  ( a = ( e +s B ) -> ( b <_s a <-> b <_s ( e +s B ) ) )
176 175 rexbidv 
 |-  ( a = ( e +s B ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) )
177 174 176 ceqsalv 
 |-  ( A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
178 177 ralbii 
 |-  ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
179 r19.23v 
 |-  ( A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
180 179 albii 
 |-  ( A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
181 173 178 180 3bitr3ri 
 |-  ( A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
182 172 181 bitri 
 |-  ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
183 eqeq1 
 |-  ( d = a -> ( d = ( A +s f ) <-> a = ( A +s f ) ) )
184 183 rexbidv 
 |-  ( d = a -> ( E. f e. ( _Right ` B ) d = ( A +s f ) <-> E. f e. ( _Right ` B ) a = ( A +s f ) ) )
185 184 ralab 
 |-  ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
186 ralcom4 
 |-  ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
187 ovex 
 |-  ( A +s f ) e. _V
188 breq2 
 |-  ( a = ( A +s f ) -> ( b <_s a <-> b <_s ( A +s f ) ) )
189 188 rexbidv 
 |-  ( a = ( A +s f ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
190 187 189 ceqsalv 
 |-  ( A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
191 190 ralbii 
 |-  ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
192 r19.23v 
 |-  ( A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
193 192 albii 
 |-  ( A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
194 186 191 193 3bitr3ri 
 |-  ( A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
195 185 194 bitri 
 |-  ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
196 182 195 anbi12i 
 |-  ( ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
197 169 196 bitri 
 |-  ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
198 138 168 197 sylanbrc 
 |-  ( ph -> A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a )
199 eqid 
 |-  ( l e. L |-> ( l +s B ) ) = ( l e. L |-> ( l +s B ) )
200 199 rnmpt 
 |-  ran ( l e. L |-> ( l +s B ) ) = { y | E. l e. L y = ( l +s B ) }
201 sltsex1 
 |-  ( L < L e. _V )
202 1 201 syl 
 |-  ( ph -> L e. _V )
203 202 mptexd 
 |-  ( ph -> ( l e. L |-> ( l +s B ) ) e. _V )
204 rnexg 
 |-  ( ( l e. L |-> ( l +s B ) ) e. _V -> ran ( l e. L |-> ( l +s B ) ) e. _V )
205 203 204 syl 
 |-  ( ph -> ran ( l e. L |-> ( l +s B ) ) e. _V )
206 200 205 eqeltrrid 
 |-  ( ph -> { y | E. l e. L y = ( l +s B ) } e. _V )
207 eqid 
 |-  ( m e. M |-> ( A +s m ) ) = ( m e. M |-> ( A +s m ) )
208 207 rnmpt 
 |-  ran ( m e. M |-> ( A +s m ) ) = { z | E. m e. M z = ( A +s m ) }
209 sltsex1 
 |-  ( M < M e. _V )
210 2 209 syl 
 |-  ( ph -> M e. _V )
211 210 mptexd 
 |-  ( ph -> ( m e. M |-> ( A +s m ) ) e. _V )
212 rnexg 
 |-  ( ( m e. M |-> ( A +s m ) ) e. _V -> ran ( m e. M |-> ( A +s m ) ) e. _V )
213 211 212 syl 
 |-  ( ph -> ran ( m e. M |-> ( A +s m ) ) e. _V )
214 208 213 eqeltrrid 
 |-  ( ph -> { z | E. m e. M z = ( A +s m ) } e. _V )
215 206 214 unexd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) e. _V )
216 snex 
 |-  { ( A +s B ) } e. _V
217 216 a1i 
 |-  ( ph -> { ( A +s B ) } e. _V )
218 23 sselda 
 |-  ( ( ph /\ l e. L ) -> l e. No )
219 8 adantr 
 |-  ( ( ph /\ l e. L ) -> B e. No )
220 218 219 addscld 
 |-  ( ( ph /\ l e. L ) -> ( l +s B ) e. No )
221 eleq1 
 |-  ( y = ( l +s B ) -> ( y e. No <-> ( l +s B ) e. No ) )
222 220 221 syl5ibrcom 
 |-  ( ( ph /\ l e. L ) -> ( y = ( l +s B ) -> y e. No ) )
223 222 rexlimdva 
 |-  ( ph -> ( E. l e. L y = ( l +s B ) -> y e. No ) )
224 223 abssdv 
 |-  ( ph -> { y | E. l e. L y = ( l +s B ) } C_ No )
225 6 adantr 
 |-  ( ( ph /\ m e. M ) -> A e. No )
226 53 sselda 
 |-  ( ( ph /\ m e. M ) -> m e. No )
227 225 226 addscld 
 |-  ( ( ph /\ m e. M ) -> ( A +s m ) e. No )
228 eleq1 
 |-  ( z = ( A +s m ) -> ( z e. No <-> ( A +s m ) e. No ) )
229 227 228 syl5ibrcom 
 |-  ( ( ph /\ m e. M ) -> ( z = ( A +s m ) -> z e. No ) )
230 229 rexlimdva 
 |-  ( ph -> ( E. m e. M z = ( A +s m ) -> z e. No ) )
231 230 abssdv 
 |-  ( ph -> { z | E. m e. M z = ( A +s m ) } C_ No )
232 224 231 unssd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) C_ No )
233 6 8 addscld 
 |-  ( ph -> ( A +s B ) e. No )
234 233 snssd 
 |-  ( ph -> { ( A +s B ) } C_ No )
235 velsn 
 |-  ( b e. { ( A +s B ) } <-> b = ( A +s B ) )
236 elun 
 |-  ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) )
237 vex 
 |-  a e. _V
238 eqeq1 
 |-  ( y = a -> ( y = ( l +s B ) <-> a = ( l +s B ) ) )
239 238 rexbidv 
 |-  ( y = a -> ( E. l e. L y = ( l +s B ) <-> E. l e. L a = ( l +s B ) ) )
240 237 239 elab 
 |-  ( a e. { y | E. l e. L y = ( l +s B ) } <-> E. l e. L a = ( l +s B ) )
241 eqeq1 
 |-  ( z = a -> ( z = ( A +s m ) <-> a = ( A +s m ) ) )
242 241 rexbidv 
 |-  ( z = a -> ( E. m e. M z = ( A +s m ) <-> E. m e. M a = ( A +s m ) ) )
243 237 242 elab 
 |-  ( a e. { z | E. m e. M z = ( A +s m ) } <-> E. m e. M a = ( A +s m ) )
244 240 243 orbi12i 
 |-  ( ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) )
245 236 244 bitri 
 |-  ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) )
246 cutcuts 
 |-  ( L < ( ( L |s R ) e. No /\ L <
247 1 246 syl 
 |-  ( ph -> ( ( L |s R ) e. No /\ L <
248 247 simp2d 
 |-  ( ph -> L <
249 248 adantr 
 |-  ( ( ph /\ l e. L ) -> L <
250 simpr 
 |-  ( ( ph /\ l e. L ) -> l e. L )
251 ovex 
 |-  ( L |s R ) e. _V
252 251 snid 
 |-  ( L |s R ) e. { ( L |s R ) }
253 252 a1i 
 |-  ( ( ph /\ l e. L ) -> ( L |s R ) e. { ( L |s R ) } )
254 249 250 253 sltssepcd 
 |-  ( ( ph /\ l e. L ) -> l
255 3 adantr 
 |-  ( ( ph /\ l e. L ) -> A = ( L |s R ) )
256 254 255 breqtrrd 
 |-  ( ( ph /\ l e. L ) -> l
257 6 adantr 
 |-  ( ( ph /\ l e. L ) -> A e. No )
258 218 257 219 ltadds1d 
 |-  ( ( ph /\ l e. L ) -> ( l  ( l +s B )
259 256 258 mpbid 
 |-  ( ( ph /\ l e. L ) -> ( l +s B )
260 breq1 
 |-  ( a = ( l +s B ) -> ( a  ( l +s B )
261 259 260 syl5ibrcom 
 |-  ( ( ph /\ l e. L ) -> ( a = ( l +s B ) -> a
262 261 rexlimdva 
 |-  ( ph -> ( E. l e. L a = ( l +s B ) -> a
263 cutcuts 
 |-  ( M < ( ( M |s S ) e. No /\ M <
264 2 263 syl 
 |-  ( ph -> ( ( M |s S ) e. No /\ M <
265 264 simp2d 
 |-  ( ph -> M <
266 265 adantr 
 |-  ( ( ph /\ m e. M ) -> M <
267 simpr 
 |-  ( ( ph /\ m e. M ) -> m e. M )
268 ovex 
 |-  ( M |s S ) e. _V
269 268 snid 
 |-  ( M |s S ) e. { ( M |s S ) }
270 269 a1i 
 |-  ( ( ph /\ m e. M ) -> ( M |s S ) e. { ( M |s S ) } )
271 266 267 270 sltssepcd 
 |-  ( ( ph /\ m e. M ) -> m
272 4 adantr 
 |-  ( ( ph /\ m e. M ) -> B = ( M |s S ) )
273 271 272 breqtrrd 
 |-  ( ( ph /\ m e. M ) -> m
274 8 adantr 
 |-  ( ( ph /\ m e. M ) -> B e. No )
275 226 274 225 ltadds2d 
 |-  ( ( ph /\ m e. M ) -> ( m  ( A +s m )
276 273 275 mpbid 
 |-  ( ( ph /\ m e. M ) -> ( A +s m )
277 breq1 
 |-  ( a = ( A +s m ) -> ( a  ( A +s m )
278 276 277 syl5ibrcom 
 |-  ( ( ph /\ m e. M ) -> ( a = ( A +s m ) -> a
279 278 rexlimdva 
 |-  ( ph -> ( E. m e. M a = ( A +s m ) -> a
280 262 279 jaod 
 |-  ( ph -> ( ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) -> a
281 245 280 biimtrid 
 |-  ( ph -> ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> a
282 281 imp 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> a
283 breq2 
 |-  ( b = ( A +s B ) -> ( a  a
284 282 283 syl5ibrcom 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> ( b = ( A +s B ) -> a
285 235 284 biimtrid 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> ( b e. { ( A +s B ) } -> a
286 285 3impia 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) /\ b e. { ( A +s B ) } ) -> a
287 215 217 232 234 286 sltsd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <
288 10 sneqd 
 |-  ( ph -> { ( A +s B ) } = { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } )
289 287 288 breqtrd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <
290 eqid 
 |-  ( r e. R |-> ( r +s B ) ) = ( r e. R |-> ( r +s B ) )
291 290 rnmpt 
 |-  ran ( r e. R |-> ( r +s B ) ) = { w | E. r e. R w = ( r +s B ) }
292 sltsex2 
 |-  ( L < R e. _V )
293 1 292 syl 
 |-  ( ph -> R e. _V )
294 293 mptexd 
 |-  ( ph -> ( r e. R |-> ( r +s B ) ) e. _V )
295 rnexg 
 |-  ( ( r e. R |-> ( r +s B ) ) e. _V -> ran ( r e. R |-> ( r +s B ) ) e. _V )
296 294 295 syl 
 |-  ( ph -> ran ( r e. R |-> ( r +s B ) ) e. _V )
297 291 296 eqeltrrid 
 |-  ( ph -> { w | E. r e. R w = ( r +s B ) } e. _V )
298 eqid 
 |-  ( s e. S |-> ( A +s s ) ) = ( s e. S |-> ( A +s s ) )
299 298 rnmpt 
 |-  ran ( s e. S |-> ( A +s s ) ) = { t | E. s e. S t = ( A +s s ) }
300 sltsex2 
 |-  ( M < S e. _V )
301 2 300 syl 
 |-  ( ph -> S e. _V )
302 301 mptexd 
 |-  ( ph -> ( s e. S |-> ( A +s s ) ) e. _V )
303 rnexg 
 |-  ( ( s e. S |-> ( A +s s ) ) e. _V -> ran ( s e. S |-> ( A +s s ) ) e. _V )
304 302 303 syl 
 |-  ( ph -> ran ( s e. S |-> ( A +s s ) ) e. _V )
305 299 304 eqeltrrid 
 |-  ( ph -> { t | E. s e. S t = ( A +s s ) } e. _V )
306 297 305 unexd 
 |-  ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) e. _V )
307 111 sselda 
 |-  ( ( ph /\ r e. R ) -> r e. No )
308 8 adantr 
 |-  ( ( ph /\ r e. R ) -> B e. No )
309 307 308 addscld 
 |-  ( ( ph /\ r e. R ) -> ( r +s B ) e. No )
310 eleq1 
 |-  ( w = ( r +s B ) -> ( w e. No <-> ( r +s B ) e. No ) )
311 309 310 syl5ibrcom 
 |-  ( ( ph /\ r e. R ) -> ( w = ( r +s B ) -> w e. No ) )
312 311 rexlimdva 
 |-  ( ph -> ( E. r e. R w = ( r +s B ) -> w e. No ) )
313 312 abssdv 
 |-  ( ph -> { w | E. r e. R w = ( r +s B ) } C_ No )
314 6 adantr 
 |-  ( ( ph /\ s e. S ) -> A e. No )
315 141 sselda 
 |-  ( ( ph /\ s e. S ) -> s e. No )
316 314 315 addscld 
 |-  ( ( ph /\ s e. S ) -> ( A +s s ) e. No )
317 eleq1 
 |-  ( t = ( A +s s ) -> ( t e. No <-> ( A +s s ) e. No ) )
318 316 317 syl5ibrcom 
 |-  ( ( ph /\ s e. S ) -> ( t = ( A +s s ) -> t e. No ) )
319 318 rexlimdva 
 |-  ( ph -> ( E. s e. S t = ( A +s s ) -> t e. No ) )
320 319 abssdv 
 |-  ( ph -> { t | E. s e. S t = ( A +s s ) } C_ No )
321 313 320 unssd 
 |-  ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) C_ No )
322 velsn 
 |-  ( a e. { ( A +s B ) } <-> a = ( A +s B ) )
323 elun 
 |-  ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) )
324 vex 
 |-  b e. _V
325 324 122 elab 
 |-  ( b e. { w | E. r e. R w = ( r +s B ) } <-> E. r e. R b = ( r +s B ) )
326 324 152 elab 
 |-  ( b e. { t | E. s e. S t = ( A +s s ) } <-> E. s e. S b = ( A +s s ) )
327 325 326 orbi12i 
 |-  ( ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) )
328 323 327 bitri 
 |-  ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) )
329 3 adantr 
 |-  ( ( ph /\ r e. R ) -> A = ( L |s R ) )
330 247 simp3d 
 |-  ( ph -> { ( L |s R ) } <
331 330 adantr 
 |-  ( ( ph /\ r e. R ) -> { ( L |s R ) } <
332 252 a1i 
 |-  ( ( ph /\ r e. R ) -> ( L |s R ) e. { ( L |s R ) } )
333 simpr 
 |-  ( ( ph /\ r e. R ) -> r e. R )
334 331 332 333 sltssepcd 
 |-  ( ( ph /\ r e. R ) -> ( L |s R )
335 329 334 eqbrtrd 
 |-  ( ( ph /\ r e. R ) -> A
336 6 adantr 
 |-  ( ( ph /\ r e. R ) -> A e. No )
337 336 307 308 ltadds1d 
 |-  ( ( ph /\ r e. R ) -> ( A  ( A +s B )
338 335 337 mpbid 
 |-  ( ( ph /\ r e. R ) -> ( A +s B )
339 breq2 
 |-  ( b = ( r +s B ) -> ( ( A +s B )  ( A +s B )
340 338 339 syl5ibrcom 
 |-  ( ( ph /\ r e. R ) -> ( b = ( r +s B ) -> ( A +s B )
341 340 rexlimdva 
 |-  ( ph -> ( E. r e. R b = ( r +s B ) -> ( A +s B )
342 4 adantr 
 |-  ( ( ph /\ s e. S ) -> B = ( M |s S ) )
343 264 simp3d 
 |-  ( ph -> { ( M |s S ) } <
344 343 adantr 
 |-  ( ( ph /\ s e. S ) -> { ( M |s S ) } <
345 269 a1i 
 |-  ( ( ph /\ s e. S ) -> ( M |s S ) e. { ( M |s S ) } )
346 simpr 
 |-  ( ( ph /\ s e. S ) -> s e. S )
347 344 345 346 sltssepcd 
 |-  ( ( ph /\ s e. S ) -> ( M |s S )
348 342 347 eqbrtrd 
 |-  ( ( ph /\ s e. S ) -> B
349 8 adantr 
 |-  ( ( ph /\ s e. S ) -> B e. No )
350 349 315 314 ltadds2d 
 |-  ( ( ph /\ s e. S ) -> ( B  ( A +s B )
351 348 350 mpbid 
 |-  ( ( ph /\ s e. S ) -> ( A +s B )
352 breq2 
 |-  ( b = ( A +s s ) -> ( ( A +s B )  ( A +s B )
353 351 352 syl5ibrcom 
 |-  ( ( ph /\ s e. S ) -> ( b = ( A +s s ) -> ( A +s B )
354 353 rexlimdva 
 |-  ( ph -> ( E. s e. S b = ( A +s s ) -> ( A +s B )
355 341 354 jaod 
 |-  ( ph -> ( ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) -> ( A +s B )
356 328 355 biimtrid 
 |-  ( ph -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( A +s B )
357 356 imp 
 |-  ( ( ph /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> ( A +s B )
358 breq1 
 |-  ( a = ( A +s B ) -> ( a  ( A +s B )
359 357 358 syl5ibrcom 
 |-  ( ( ph /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> ( a = ( A +s B ) -> a
360 359 ex 
 |-  ( ph -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( a = ( A +s B ) -> a
361 360 com23 
 |-  ( ph -> ( a = ( A +s B ) -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a
362 322 361 biimtrid 
 |-  ( ph -> ( a e. { ( A +s B ) } -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a
363 362 3imp 
 |-  ( ( ph /\ a e. { ( A +s B ) } /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> a
364 217 306 234 321 363 sltsd 
 |-  ( ph -> { ( A +s B ) } <
365 288 364 eqbrtrrd 
 |-  ( ph -> { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } <
366 18 108 198 289 365 cofcut1d 
 |-  ( ph -> ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )
367 10 366 eqtrd 
 |-  ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )